CODEWITHSUNDEEP
haskelltypeslambda-calculushigher-kinded-typestype-theory
crunch
crunch

Reputation: 166

Implementing nested/recursive datatypes in the presence of type operators

I've been working on my implementation of System F-omega in Rust following Pierce's Types and Programming Languages, and I'm looking for guidance on adding recursive types to my implementation using iso-recursive fold/unfold operators. I have already added in sum, product, record, existential, and universal types.

In System F (w/o type operators), I found it relatively straightforward to do, and I just had a visitor pass through the AST after parsing to perform the fold/unfold isomorphism during case analysis or type construction.

With System F omega, the situation is somewhat more complicated due to the presence of lambda abstractions at the type level. For example (using standard lambda-calc/haskell-ish syntax), lets say I want to define a parameterized List datatype

datatype List a = Cons a (List a) | Nil

This can be encoded in our calculi as (omitting * kinds):

type List = μ ΛX::*=>*. ΛA. Cons A (X A) | Nil
substs to: ΛA. Cons A ((μ ΛX::*=>*. ΛA. Cons A (X A) | Nil) A) | Nil

But this has issues as soon as we try to unfold the value, since a new abstraction trying to bind A again is introduced. This seems like it could work, as long as we are storing the concrete type A somewhere.

Or we can 'lambda drop' it to:

type ListF = ΛX. ΛA. Cons (A, X) | Nil
type List  = ΛA. μ (ListF A)

The lambda dropping works well for simple recursive types like this, and is straightforward to implement as well, and I can envision a way to automatically generate the ListF type. But I have a nagging feeling that something is off about this.

I have been trying to read the literature around this (Mendler-style iteration, Andreas Abel, Ralph Matthes, Tarmo Uustalu, "Iteration and coiteration schemes for higher-order and nested datatypes", etc), but tbh some of it is a bit over my head, and I'm lost as to how to actually implement this in a concrete manner. Any advice would be greatly appreciated

Upvotes: 3

Views: 184

Answers (1)

HTNW
HTNW

Reputation: 29193

List = μ ΛX. ΛA. Cons A (X A) | Nil
-- μF unfolds to F(μF)
= (ΛX. ΛA. Cons A (X A) | Nil) (μ ΛX. ΛA. Cons A (X A) | Nil)
-- substitute *correctly*
= ΛA. Cons A ((μ ΛX. ΛA. Cons A (X A) | Nil) A) | Nil
--                                           ^ you dropped this!
-- folding back
List = ΛA. Cons A (List A) | Nil

The A does not need to be "stored" anywhere except the type itself. You dropped the application containing it when it should not have been dropped. Notice that your unfolding is ill-kinded. The second field of the top-level Cons has kind * => *, but that's not right. But the original was well-kinded, so the unfolding (which should preserve kinds) must have gone wrong.

"Lambda dropping" is fine, but it's not always possible. Consider

data Binary a = Leaf a | Branch (Binary (a, a))

which contains precisely 2^n as for some natural n. This type is irregularly recursive and cannot be expressed in terms of μ :: (* => *) => * as List can.

type Binary = μ ΛX. ΛA. Leaf A | Branch (X (A, A))

Upvotes: 4

Related Questions