[Ur] First-Class Polymorphism example

[Adam Chlipala]

Marc Weber wrote:
> http://impredicative.com/ur/tutorial/tlc.html
> shows this example:
>
>    type nat = t :: Type ->  t ->  (t ->  t) ->  t
>    val zero : nat = fn [t :: Type] (z : t) (s : t ->  t) =>  z
>    fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t ->  t) =>  s (n [t] z s)
>
>    val one = succ zero
>    val two = succ one
>    val three = succ two
>
>    three [int] 0 (plus 1)
>    == 3
>
>    three [string] "" (strcat "!")
>    == "!!!"
>
> Eg the succ function has t in its return type and in it n:nat arg.
> So should urweb be able to deduce type of t automatically? Should it be
> possible to replace the explicit :: by an implicit t ::: Type ?
>
> Trying to do so I get some unification errors - is it because I removed
> some [t] like args incorrectly?

You're not far from a correct solution.  You just need to use [@@] 
prefixes to suppress implicit argument insertion in places where you 
want to retain first-class polymorphism.

type nat = t ::: Type -> t -> (t -> t) -> t
val zero : nat = fn [t ::: Type] (z : t) (s : t -> t) => z
fun succ (n : nat) : nat = fn [t ::: Type] (z : t) (s : t -> t) => s (n z s)

val one = @@succ @@zero
val two = @@succ @@one
val three = @@succ @@two

val test1 = three 0 (plus 1)
val test2 = three "" (strcat "!")