Recursive Types
In order for us to have more advanced data types, we need to allow them to be recursive. Unfortunately, this opens up a whole host of problems, namely the posibility of an infinitely deep type (type a = type a). In order to mitigate this, we introduct fold and unfold which pack and unpack a recursive type respectively. Let's consider a traditional definition of a list
alias clist = rec l. < `Nil unit + `Cons { `Data int * `Prev l } > in
alias list = < `Nil unit + `Cons { `Data int * `Prev clist } > in
fold as clist
`Cons { `Data 3, `Prev (
fold as clist
`Cons { `Data 2, `Prev (
fold as clist
`Cons { `Data 1, `Prev (
fold as clist (`Nil () as list)
)} as list
)} as list
)} as list
Recursion
Now given that list, how can we add up all of its elements and return the value? To do this, we also need a recursive function. For this, we use a fixed point function.
alias clist = rec l. < `Nil unit + `Cons { `Data int * `Prev l } > in
alias list = < `Nil unit + `Cons { `Data int * `Prev clist } > in
(
fix f list: clist returns int.
case (unfold list) {
`Nil u -> 0
| `Cons r -> r#`Data + (f r#`Prev)
}
)(
fold as clist
`Cons { `Data 3, `Prev (
fold as clist
`Cons { `Data 2, `Prev (
fold as clist
`Cons { `Data 1, `Prev (
fold as clist (`Nil () as list)
)} as list
)} as list
)} as list
)
Thanks!
This covers a lot of the important bits of System F. Play around with it and see what you can do!