2021-09-08 20:01:40 +03:00
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:
2024-07-10 17:46:18 +03:00
``` unison
2021-09-08 20:01:40 +03:00
f : (forall a . a -> a) -> (Nat, Text)
f id = (id 1, id "hi")
> f (x -> x)
```
2024-07-10 19:17:15 +03:00
``` ucm
2021-09-08 20:01:40 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2021-09-08 20:01:40 +03:00
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}` :
2024-07-10 17:46:18 +03:00
``` unison
2024-07-01 20:28:52 +03:00
f : (forall a g . '{g} a -> '{g} a) -> () -> ()
f id _ =
2022-12-02 08:51:11 +03:00
_ = (id ('1 : '{} Nat), id ('("hi") : '{IO} Text))
2021-09-08 20:01:40 +03:00
()
```
2024-07-10 19:17:15 +03:00
``` ucm
2021-09-08 20:01:40 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2021-09-08 20:01:40 +03:00
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:
2024-07-10 17:46:18 +03:00
``` unison
2021-09-08 20:01:40 +03:00
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 -> ()
2024-07-01 20:28:52 +03:00
Functor.blah = cases Functor f ->
2021-09-08 20:01:40 +03:00
g : forall a b . (a -> b) -> f a -> f b
g = f
()
```
2024-07-10 19:17:15 +03:00
``` ucm
2021-09-08 20:01:40 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2021-09-08 20:01:40 +03:00
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` :
2024-01-04 11:42:12 +03:00
type Functor f
2021-09-08 20:01:40 +03:00
Functor.blah : Functor f -> ()
Functor.map : Functor f
-> (∀ a b. (a -> b) -> f a -> f b)
```
2024-07-01 20:28:52 +03:00
This example is similar, but involves abilities:
2021-09-08 20:01:40 +03:00
2024-07-10 17:46:18 +03:00
``` unison
2023-09-20 19:08:02 +03:00
unique ability Remote t where doRemoteStuff : t ()
2024-07-01 20:28:52 +03:00
unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a)
2021-09-08 20:01:40 +03:00
Loc.blah : Loc -> ()
Loc.blah = cases Loc f ->
f0 : '{Remote tx} ax ->{Remote tx} tx ax
f0 = f
()
2024-07-01 20:28:52 +03:00
-- In this case, no annotation is needed since the lambda
2021-09-08 20:01:40 +03:00
-- is checked against a polymorphic type
2024-07-01 20:28:52 +03:00
Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a)
2021-09-08 20:01:40 +03:00
-> 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
2024-07-01 20:28:52 +03:00
Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a)
2021-09-08 20:01:40 +03:00
-> Loc -> Loc
2024-07-01 20:28:52 +03:00
Loc.transform2 nt = cases Loc f ->
2021-09-08 20:01:40 +03:00
f' : forall t a . '{Remote t} a ->{Remote t} t a
f' a = f (nt a)
2024-07-01 20:28:52 +03:00
Loc f'
2021-09-08 20:01:40 +03:00
```
2024-07-10 19:17:15 +03:00
``` ucm
2021-09-08 20:01:40 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2021-09-08 20:01:40 +03:00
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` :
2024-01-04 11:42:12 +03:00
type Loc
ability Remote t
2021-09-08 20:01:40 +03:00
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
```
2022-02-09 23:15:26 +03:00
## Types with polymorphic fields
2024-07-10 17:46:18 +03:00
``` unison
2022-02-09 23:15:26 +03:00
structural type HigherRanked = HigherRanked (forall a. a -> a)
```
We should be able to add and view records with higher-rank fields.
2024-07-10 19:17:15 +03:00
``` ucm
2024-07-01 20:28:52 +03:00
scratch/main> add
2022-02-09 23:15:26 +03:00
⍟ I've added these definitions:
structural type HigherRanked
2024-07-01 20:28:52 +03:00
scratch/main> view HigherRanked
2022-02-09 23:15:26 +03:00
structural type HigherRanked = HigherRanked (∀ a. a -> a)
```