This transcript does some testing of higher-rank types. Regression tests related to higher-rank types can be added here. In this example, a higher-rank function is defined, `f`. No annotation is needed at the call-site of `f`, because the lambda is being checked against the polymorphic type `forall a . a -> a`, rather than inferred: ``` unison f : (forall a . a -> a) -> (Nat, Text) f id = (id 1, id "hi") > f (x -> x) ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: f : (∀ a. a ->{g} a) ->{g} (Nat, Text) Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels. 4 | > f (x -> x) ⧩ (1, "hi") ``` Another example, involving abilities. Here the ability-polymorphic function is instantiated with two different ability lists, `{}` and `{IO}`: ``` unison f : (forall a g . '{g} a -> '{g} a) -> () -> () f id _ = _ = (id ('1 : '{} Nat), id ('("hi") : '{IO} Text)) () ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: f : (∀ a g. '{g} a ->{h} '{g} a) -> '{h} () ``` Here's an example, showing that polymorphic functions can be fields of a constructor, and the functions remain polymorphic even when the field is bound to a name during pattern matching: ``` unison unique type Functor f = Functor (forall a b . (a -> b) -> f a -> f b) Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b) Functor.map = cases Functor f -> f Functor.blah : Functor f -> () Functor.blah = cases Functor f -> g : forall a b . (a -> b) -> f a -> f b g = f () ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: type Functor f Functor.blah : Functor f -> () Functor.map : Functor f -> (∀ a b. (a -> b) -> f a -> f b) ``` This example is similar, but involves abilities: ``` unison unique ability Remote t where doRemoteStuff : t () unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a) Loc.blah : Loc -> () Loc.blah = cases Loc f -> f0 : '{Remote tx} ax ->{Remote tx} tx ax f0 = f () -- In this case, no annotation is needed since the lambda -- is checked against a polymorphic type Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a) -> Loc -> Loc Loc.transform nt = cases Loc f -> Loc (a -> f (nt a)) -- In this case, the annotation is needed since f' is inferred -- on its own it won't infer the higher-rank type Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a) -> Loc -> Loc Loc.transform2 nt = cases Loc f -> f' : forall t a . '{Remote t} a ->{Remote t} t a f' a = f (nt a) Loc f' ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: type Loc ability Remote t Loc.blah : Loc -> () Loc.transform : (∀ t a. '{Remote t} a -> '{Remote t} a) -> Loc -> Loc Loc.transform2 : (∀ t a. '{Remote t} a -> '{Remote t} a) -> Loc -> Loc ``` ## Types with polymorphic fields ``` unison structural type HigherRanked = HigherRanked (forall a. a -> a) ``` We should be able to add and view records with higher-rank fields. ``` ucm scratch/main> add ⍟ I've added these definitions: structural type HigherRanked scratch/main> view HigherRanked structural type HigherRanked = HigherRanked (∀ a. a -> a) ```