[CakeML] Polymorphic type annotation

[Scott Owens]

At the moment, type variables are not allowed in type annotations. Even though you can’t write the type annotation down, the function can still be polymorphic if you leave the annotation off.

Of course, you’ll notice that the type error message there isn’t so good. In general, we need to improve them.

Scott

> On 2018/05/02, at 09:59, Mário Pereira <Mario.Parreira-Pereira at lri.fr> wrote:
> 
> Dear list,
> 
> I am currently running some experiences around the CakeML compiler.
> 
> I ran across some difficulties when trying to annotate function arguments with polymorphic types. Take for instance the CPS version of a function that computes the height of a binary tree:
> 
> datatype 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
> 
> fun height t (k: int -> int) =
>  case t of
>    Leaf => k 0
>  | Node l _ r =>
>      height l (fn hl =>
>      height r (fn hr => 1 + max hl hr))
> 
> This program is accepted by CakeML. However, I would like to write the following more general version of it:
> 
> fun height t (k: int -> 'a) =
>  case t of
>    Leaf => k 0
>  | Node l _ r =>
>      height l (fn hl =>
>      height r (fn hr => 1 + max hl hr))
> 
> which gives me "### ERROR: type error Bad type annotation in pattern".  I see the error is not related to the arrow type, as the polymorphic identity function 'fun id (x: 'a) = x' is also rejected.
> 
> Am I doing something wrong with the syntax of type annotations ?
> 
> Best regards
> --
> Mário Pereira
> 
> 
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users