{- Various random examples and sample code -} {- an abbreviation for -} let LTypeable = ; {- types defined using 'let' are _not_ names: they are exactly equivalent to their structure. -} let Option_struct = \A:*.{ lJust of A | lNothing }; {- Some mutually recursive types -} new lCompany : * = { lC of (llist lDept) } and lDept : * = { lD of (lName * lManager * (llist lSubUnit)) } and lSubUnit : * = { lPU of lEmployee | lDU of lDept } and lEmployee: * = { lE of (lPerson * lSalary) } and lPerson : * = { lP of (lName * lAddress) } and lSalary : * = { lS of Int } and lManager : * = lEmployee and lName : * = Int and lAddress : * = Int and lOption : * -> * = \A:*.{ lJust of A | lNothing } {- And here are the labels they mention -} in let LTypes = {- Just for the sake of convenience we define a polymorphic function nothing and a polymorphic function some to serve as constructors for Option_struct things. Note that in order to typecheck variant expressions, they have to be annotated with the type they belong to (otherwise this would be ambiguous (Ocaml resolves the similar problem by not allowing variants to share label names in the same modules. We might adopt this approach later, but it seems restrictive. Anyway ...) -} in let nothing = \Ls:LABS.\B:*|Ls. (lNothing():(Option_struct B)) in let some = \Ls:LABS.\B:*|Ls.\x:B. lJust(x):(Option_struct B) {- A _very_ cool example of how typecase can be used to compare two labels as part of a type-safe cast operation! -} in let xlblCmp ={- first take two labels of kind * -} \lA:LAB(*),lB:LAB(*). {- analyse the first label, as if it were a type (remember: labels can be considered as types everywhere!) -} typecase lA of { {- now, because lA viewed as a type, trivially contains lA, we must provide a case for it. When lB is not instantiated to what lA is instantiated this branch will be taken and the function will return nothing, that is, the cast will fail. -} lA => \x:lA. nothing [] [lB] : \A:*. A -> (Option_struct lB) | , {- on the other hand, when lB is instantiated to exactly what lA is, then we actually have two matching branches!!! BUT, the semantics of the language say that the right-most wins, returning thus some value :-D -} lB => \x:lB. some [] [lB] x : \A:*. A -> (Option_struct lB) | } {- Here's for example a failing cast! :-D -} in let w = xlblCmp lint lbool 3 {- Every examples bundle must have some easy to follow examples, as well -} in let apply_f = \A:*|LTypes,B:*|LTypes. \f:[lB:LAB(*)].A -> (Option_struct lB). typecase B of { lCompany => f lCompany : \B:*.A -> (Option_struct B) | LTypes, lDept => f lDept : \B:*.A -> (Option_struct B) | LTypes, lSubUnit => f lSubUnit : \B:*.A -> (Option_struct B) | LTypes, lEmployee => f lEmployee : \B:*.A -> (Option_struct B) | LTypes, lPerson => f lPerson : \B:*.A -> (Option_struct B) | LTypes, lSalary => f lSalary : \B:*.A -> (Option_struct B) | LTypes, lManager => f lManager : \B:*.A -> (Option_struct B) | LTypes, lName => f lName : \B:*.A -> (Option_struct B) | LTypes, lAddress => f lAddress : \B:*.A -> (Option_struct B) | LTypes, lint => f lint : \B:*.A -> (Option_struct B) | LTypes } {- Nothing interesting here -} in let xcast = fix cast:[A:*| LTypes, B:*| LTypes]. A -> (Option_struct B). \A:*| LTypes, B:*| LTypes. typecase A of { lCompany => apply_f [lCompany] [B] (xlblCmp lCompany) : \A:*.A -> (Option_struct B) | LTypes, lDept => apply_f [lDept] [B] (xlblCmp lDept) : \A:*.A -> (Option_struct B) | LTypes, lSubUnit => apply_f [lSubUnit] [B] (xlblCmp lSubUnit) : \A:*.A -> (Option_struct B) | LTypes, lEmployee => apply_f [lEmployee] [B] (xlblCmp lEmployee) : \A:*.A -> (Option_struct B) | LTypes, lPerson => apply_f [lPerson] [B] (xlblCmp lPerson) : \A:*.A -> (Option_struct B) | LTypes, lSalary => apply_f [lSalary] [B] (xlblCmp lSalary) : \A:*.A -> (Option_struct B) | LTypes, lManager => apply_f [lManager] [B] (xlblCmp lManager) : \A:*.A -> (Option_struct B) | LTypes, lName => apply_f [lName] [B] (xlblCmp lName) : \A:*.A -> (Option_struct B) | LTypes, lAddress => apply_f [lAddress] [B] (xlblCmp lAddress) : \A:*.A -> (Option_struct B) | LTypes, lint => apply_f [lint] [B] (xlblCmp lint) : \A:*.A -> (Option_struct B) | LTypes } in let y = some [LTypeable] [Int] 3 in let z = nothing [LTypeable] [Int] {- Something more interesting: A type-safe cast for types mentioning labels in LTypeable -} in let ecast = {- the type of cast: take two types mentioning labels in LTypeable, take an element of the first type and convert it to sth that is Option_struct of the second type. -} fix cast:[A:*| LTypeable,B:*|LTypeable]. A -> (Option_struct B). {- abstract over the types -} \A:*|LTypeable,B:*|LTypeable. typecase A of { {- if A is int -} lint => typecase B of { {- if B is int then we are okay -} lint => \x:Int. (some [LTypeable] [Int] x) : \B:*. Int -> (Option_struct B) | LTypeable, {- if B is product, no! -} lproduct => \B1:*|LTypeable,B2:*|LTypeable. \x:Int. nothing [LTypeable] [(B1*B2)] : \B:*.Int -> (Option_struct B) | LTypeable } : \A:*.A -> (Option_struct B) | LTypeable, {- of A is product, then fist abstract the types of the product, as indicated by lproduct kind (*->*->*) -} lproduct => \A1:*|LTypeable,A2:*|LTypeable. typecase B of { {- if B is a product, essentially try to cast the subcomponents -} lproduct => \B1:*|LTypeable,B2:*|LTypeable. \x:A1*A2. match (cast [A1] [B1] x.fst) with {- do a small pattern matching -} lJust(x1) -> begin match (cast [A2] [B2] x.snd) with lNothing(_) -> nothing [LTypeable] [(B1*B2)] | lJust(x2) -> some [LTypeable] [(B1*B2)] (x1,x2) end | lNothing(_) -> nothing [LTypeable] [(B1*B2)] : \B:*.(A1*A2) -> (Option_struct B) | LTypeable, {- if B is int, fail -} lint => \x:A1*A2. nothing [LTypeable] [Int] : \B:*.(A1*A2) -> (Option_struct B) | LTypeable } : \A:*.A -> (Option_struct B) | LTypeable } {- Here's a fancy higher-order based type-safe cast, taken from Weirich's functional pearl. The trick is here to abstract over a constructor C -} in let ecastHo = {- as before, take A,B but also take a constructor C of kind * -> * now, the function will take sth that is C A and try to cast it to C B. Initially it will be called with the identity constructor -} fix cast:[A:*|LTypeable,B:*|LTypeable,C:*->*|LTypeable]. (C A) -> Option_struct (C B). \A:*|LTypeable,B:*|LTypeable,C:*->*|LTypeable. typecase A of { {- easy cases, when A is integer -} lint => typecase B of { lint => \x:(C Int). some [LTypeable] [C Int] x : \B:*.(C Int) -> (Option_struct (C B)) | LTypeable, lproduct => \B1:*|LTypeable,B2:*|LTypeable. \x:(C Int). nothing [LTypeable] [C (B1*B2)] : \B:*.(C Int) -> (Option_struct (C B)) | LTypeable } : \A:*. (C A) -> (Option_struct (C B)) | LTypeable, {- if it is product, first abstract A1 and A2 as the kind of lproduct suggests (*->*->*) -} lproduct => \A1:*|LTypeable,A2:*|LTypeable. typecase B of { {- if B is int, the case is not interesting; just fail -} lint => \x:C (A1*A2). nothing [LTypeable] [C Int] : \B:*.(C (A1*A2)) -> (Option_struct (C B)) | LTypeable, {- if B is product, first abstract B1 and B2 -} lproduct => \B1:*|LTypeable,B2:*|LTypeable. {- create a function that will cast the first component of a product inside the C constructor -} let f = cast [A1] [B1] [\D:*. C (D*A2)] in {- create a function that will cast the second component of the semi-converted type that the first will return! -} let g = cast [A2] [B2] [\D:*. C (B1*D)] in {- now, take x and try to apply f and g to it! No destructive casts any more! -} \x:C (A1*A2). match f x with lNothing(_) -> nothing [LTypeable] [C (B1*B2)] | lJust(y) -> begin match g y with lNothing(_) -> nothing [LTypeable] [C (B1*B2)] | lJust(z) -> some [LTypeable] [C (B1*B2)] z end : \B:*.(C (A1*A2)) -> (Option_struct (C B)) | LTypeable } : \A:*. (C A) -> (Option_struct (C B)) | LTypeable } in ()