Skip to content

Addition of iso recursive types to System F omega

Jump to bottom
Michael Lazear edited this page Dec 6, 2019 · 7 revisions

Given a simple System F omega calculus:

Kinds (K, L)  ::= * 
				| K => L

Types (T, U)  ::= Unit
				| X			-- type variable
				| T -> U 		-- type of functions
				| forall X :: K. T 	-- universal type
				| \X::K. T		-- type abstraction
				| T U			-- type application

Terms (t, u)  ::= unit
				| x 			-- variable
				| (\x: T. t)		-- abstraction
				| t u 			-- application
				| \X::K. t 		-- term-level type abstraction
				| t [T] 		-- term-level type application

Addition of iso-recursive types:

Types (T, U)  ::= ...
				| μ X. T 

Terms (t, u)  ::= ...
				| fold (mu X. T) t
				| unfold (mu X. T) t

We can easily represent a NatList as an iso-recursive type in this system:

type NatList = Cons (Nat, NatList) | Nil  :: μ NatList. Cons (Nat, Var(0)) | Nil -- using de Bruijn indices

which would unfold into:

Cons (Nat, μ Cons(Nat, μ Cons (Nat, Var(0) | Nil)) | Nil

How can we represent a higher-kinded List?

type List 'a = Cons ('a, List 'a) | Nil

The first pass is to represent this as a recursive type with a type operator:

μ List. \A :: *. Cons (A, List A) | Nil

If we apply a unfold first, we yield the following. We will have to repeatedly apply a type (say, Nat)

ΛA :: *. Cons(A, μ List. \A :: *. Cons (A, List A) | Nil) | Nil

What if we represent this first as a type operator with a body that is a recursive type?

type List = ΛA::*. μ ListF. Cons(A, ListF) | Nil
μ ListF. Cons(Nat, ListF) | Nil

This works, but it won't work for a perfect tree

type Tree a = Leaf a | Tree (a, a)

type Tree = ΛA::*. μ TreeF. Leaf A | TreeF (A, A)
=> μ TreeF. Leaf Nat | TreeF (Nat, Nat)

Resources:

Clone this wiki locally