Recursive types

[xsebek]

Add a rec (like Fix) operator which would open the door to any recursive data structure, like list, set or map.

This would also add two reserved function names:

• roll : f (rec f) -> rec f
• unroll : rec f -> f (rec f)

Example from IRC (lets assume a + b = L a | R b, and functions getLeft, getRight):

type listf a b = () + a * b end
type list a = rec (listf a) end

def nil  : list a           = roll (L ()) end
def cons : a -> list a      = \x. \xs. roll (R (x,xs)) end
def head : list a -> a      = \xs. fst (getRight (unroll xs)) end
def tail : list a -> list a = \xs. snd (getRight (unroll xs)) end

> let l = cons 1 (cons 2 (cons 3 nil)) in head l, tail l
(1, cons 2 (cons 3 nil)) : int * rec 

Special case for list

As the list is particularly useful it might be provided to players early and internally stored as rec, with special rules for parsing and pretty-printing. Something like [1,2,3] and hardcoding the type synonym list.
In gameplay, this could be introduced as a "stable form" of something more advanced. Having the appropriate device installed would load the basic list functions into the dictionary. Curious players could then type > cons and wonder what it will later be useful for. 🙂

Related:

• would require Add type synonyms (or just generalize to System Fω) #153 to get the rec applied to correct types
• Add sum types to the language #46 to make it useful (though there is the magical streamf a = (int, () -> a))
• Change run to import and typecheck it properly #495 (so less savvy players could load data.list.sw which they would find on Wiki)

[byorgey]

Some additional thoughts:

• Instead of having rec be a type operator, like Fix in Haskell, it's probably more flexible to have it bind a type variable. For example, instead of

  type listf a b = () + a * b end
  type list a = rec (listf a) end
  

  we could just write

  type list a = rec l. () + a * l end
  

  This way we don't have to go into contortions to always define a "structure functor" with a type variable representing recursive occurrences as the last parameter.
• It might not be necessary to hardcode the type synonym list. It might be more fun to just have the built-in syntax work directly with rec l. () + a * l, and implement equality checking for types (in this case I think only alpha-equivalence would be needed), so that built-in list things are compatible with the user's type synonym.
• We might also consider implementing equirecursive types instead of isorecursive types. In brief,
  • With equirecursive types, we could have e.g. list a = () + a * list a, where the left- and right-hand sides are completely interchangeable. In other words, recursive type synonyms (Haskell does not have this!). So no roll and unroll operations are needed. For example, cons : a -> list a -> list a = \x. \xs. inr (x,xs) would be well-typed in such a system.
  • This means that equality testing for types becomes much more interesting. We can no longer tell just by looking whether two types are the same. However, type equality is still decidable via coinduction: keep unrolling the types being compared and matching up their components, failing if we ever discover an incompatible pair of types, and stopping the recursion whenever we see a pair of types we have seen before.
  • The implementation would be more complex but it would be nicer for users in some way since no roll and unroll would be required (although it could perhaps be more confusing for the same reason).
• With isorecursive types, on the other hand, list a = rec l. () + a * l is not the same type as () + a * list l, but they are related by roll/unroll.
  • This makes the implementation much easier: type equality testing is trivial. But code is noisier due to the need for explicit rec operator in types and roll and unroll in terms.

[xsebek]

@byorgey the equirecursive types look cool, but the paper about them in F-omega system seems a bit too powerful for Swarm. 😮

I like the rec binding a type variable suggestion, as that seems easier to implement in the current type system. 👍

If I understand correctly, it is not even blocked on type synonyms (#153), though it would be annoying to use without them.

But what would the types of functions change to? 🤔

[byorgey]

@byorgey the equirecursive types look cool, but the paper about them in F-omega system seems a bit too powerful for Swarm. 😮

Well, we don't have System F-omega, just System F.

If I understand correctly, it is not even blocked on type synonyms (#153), though it would be annoying to use without them.

Agreed.

But what would the types of functions change to? 🤔

What do you mean? Why would the types of functions change?

[xsebek]

Well if rec works like type list a = rec l. () + a * l end, would the definitions of roll/unroll need to change?