Examples
id = %L %a. %l x:%a.x
id : \A %a. %a -> %a
twice1 = %L %a.%l f: %L %b. %b -> %b. %l x:%a. f[%a](f[%a](x))
twice1 : \A %a. \A %b. (%b -> %b) -> %a -> %b
twice2 = %L %a.%l f: %a -> %a. %l x:%a. f(f(x))
twice2 : \A %a. (%a -> %a) -> %a -> %a
Applications
id [ Int ] ( 3 ) = 3
twice1 [ Int ] ( id )( 3 ) = 3
twice1 [ Int ] ( S ) = illegal
twice2 [ Int ] ( S )( 3 ) = 5
slide
:
Parametrized types -- examples
