With Variant, we get extensible sums, but one drawback is you can’t have recursive data types. If you try to use recursion with type synonyms and records, you’ll get an error. The compiler would attempt to expand the recursive alias into an infinite type. The same restriction applies to Variant.
type List a = Variant (nil :: Unit, cons :: Tuple a (List a))
We would have to newtype this, which defeats the point, since we lose extensibility. However, with VariantF we can utilize fixed-point combinators to introduce a recursive variant.
type NIL r = (nil :: FProxy (Const Unit) | r)
type CONS a r = (cons :: FProxy (Tuple a) | r)
type ListF r a = VariantF (NIL + CONS a + r)
type List r a = Mu (LiftF r a)
This gives us a self-recursive extensible data type. But often times (like when writing types for language ASTs), we actually want mutually recursive data types. As an example, here is a small AST for adding numbers that also support let bindings. We’ve separated Binding out into a different data type because we might want to add more than 1 binding form.
data Expr
= Lit Int
| Var String
| Add Expr Expr
| Let Binding Expr
data Binding
= Bound String Expr
For a language like PureScript, there are several such data types that form its mutually recursive AST. So now, why does the Mu VariantF approach fall flat with something like this? Translating Add is straightforward:
data Add a = Add a a
type ADD r = (add :: FProxy Add | r)
derive instance functorAdd :: Functor Add
But if you look at something like Let, it discriminates two points of recursion (Expr and Binding) which forms a mutual binding group. A naive attempt to translate Let is clearly wrong:
data Let a = Let a a
Since we are only using one variable a, it would be self-recursive in both arguments. We could potentially add two variables for each point of recursion:
data Let a b = Let a b
But this has a different kind, and does not fit uniformly into our framework. Since the particular branch we want to take in our binding group is determined by argument position, all of our data types would have to have the same number of arguments, and use the same slots to represent each data type. That means if we wanted to add another branch, then we’d have to go back and change all the data types. Not very extensible!
We can refactor this though and get something that is both uniform and can give us an infinite supply of types. At the value level, say we have a function that takes two arguments:
foo :: Int -> Int -> Unit
This is essentially a product (Int * Int). We can refactor this using an exponent (Int^2). In the algebra of data types, this is the -> operator. We just need a type with 2 inhabitants: Boolean = True | False.
foo :: (Boolean -> Int) -> Unit
So now instead of taking two parameter, I can take a single function parameter and feed it an index (true or false) to get a value for a particular branch. We can apply this same trick to our functor families, and since we ultimately want to use Variant, we will index it by Symbols.
data Add f = Add (f (SProxy "expr")) (f (SProxy "expr"))
data Let f = Let (f (SProxy "binding")) (f (SProxy "expr"))
Or, in a prettier way:
type Expr f = f (SProxy "expr")
type Binding f = f (SProxy "binding")
data Add f = Add (Expr f) (Expr f)
data Let f = Let (Binding f) (Expr f)
However, now our type parameter is of kind Type -> Type instead of Type, so we need a different abstraction than Functor.
class NFunctor f where
nmap :: forall a b. (a ~> b) -> f a -> f b
Where we use a natural transformation (~>) between functors. Implementing this is mostly just boilerplate for our data types.
data NFProxy (f :: (Type -> Type) -> Type) = NFProxy
type Expr f = f (SProxy "expr")
type Binding f = f (SProxy "binding")
data Lit (f :: Type -> Type) = Lit Int
type LIT r = (lit :: NFProxy Lit | r)
instance nfunctorLit :: NFunctor Lit where nmap f (Lit a) = Lit a
data Var (f :: Type -> Type) = Var String
type VAR r = (var :: NFProxy Var | r)
instance nfunctorVar :: NFunctor Var where nmap f (Var a) = Var a
data Add f = Add (Expr f) (Expr f)
type ADD r = (add :: NFProxy Add | r)
instance nfunctorAdd :: NFunctor Add where nmap f (Add a b) = Add (f a) (f b)
data Let f = Let (Binding f) (Expr f)
type LET r = (let :: NFProxy Let | r)
instance nfunctorLet :: NFunctor Let where nmap f (Let a b) = Let (f a) (f b)
data Bound f = Bound String (Expr f)
type BOUND r = (bound :: NFProxy Bound | r)
instance nfunctorBound :: NFunctor Bound where nmap f (Bound a b) = Bound a (f b)
With this we can start assembling a new Variant type for this shape:
data VariantNF (r :: # Type) (f :: Type -> Type)
inj ::
forall r rx sym f a.
Row.Cons sym (NFProxy f) rx r =>
IsSymbol sym =>
NFunctor f =>
SProxy sym ->
f a ->
VariantNF r a
lit :: forall f r. Int -> VariantNF (LIT + r) f
lit = inj (SProxy :: SProxy "lit") <<< Lit
var :: forall f r. String -> VariantNF (VAR + r) f
var = inj (SProxy :: SProxy "var") <<< Var
add :: forall f r. Expr f -> Expr f -> VariantNF (ADD + r) f
add a b = inj (SProxy :: SProxy "add") $ Add a b
letIn :: forall f r. Binding f -> Expr f -> VariantNF (LET + r) f
letIn a b = inj (SProxy :: SProxy "let") $ Let a b
bound :: forall f r. String -> Expr f -> VariantNF (BOUND + r) f
bound a b = inj (SProxy :: SProxy "bound") $ Bound a b
So far this is mostly the same as normal VariantF, just with a different kind. Now we can implement a new fixpoint type which lets us tie the mutual binding group together, much like what Mu does for VariantF. We are going to index it by our binding identifiers, in the same vein as Variant.
data Tied (r :: # Type) a
tie ::
forall r rx rec sym.
Row.Cons sym (RProxy r) rx rec =>
SProxy sym ->
VariantNF r (Tied rec) ->
Tied rec (SProxy sym)
untie ::
forall r rx rec sym.
Row.Cons sym (RProxy r) rx rec =>
Tied rec (SProxy sym) ->
VariantNF r (Tied rec)
This Tied type takes the spine for the entire binding group, and fixes it to a particular branch, as indicated by the SProxy argument.
type EXPR f r = (expr :: RProxy f | r)
type BINDING f r = (binding :: RProxy f | r)
expr ::
forall f r.
VariantNF f (Tied (EXPR f + r)) ->
Tied (EXPR f + r) (SProxy "expr")
expr = tie (SProxy :: SProxy "expr")
binding ::
forall f r.
VariantNF f (Tied (BINDING f + r)) ->
Tied (BINDING f + r) (SProxy "binding")
binding = tie (SProxy :: SProxy "binding")
And with this we can build our mutually recursive tree.
test :: _
test =
expr
(letIn
(binding
(bound "foo"
(expr (lit 42))))
(expr
(add
(expr (var "foo"))
(expr (lit 42)))))
Which infers beautifully.
Wildcard type definition has the inferred type
Tied
( expr :: RProxy
( "let" :: NFProxy Let
, add :: NFProxy Add
, lit :: NFProxy Lit
, var :: NFProxy Var
| t0
)
, binding :: RProxy
( bound :: NFProxy Bound
| t1
)
| t2
)
(SProxy "expr")
The NFunctor type is suspiciously similar to the more general and known HFunctor:
class HFunctor f where
hmap :: forall a b. (a ~> b) -> f a ~> f b
Where f is (Type -> Type) -> Type -> Type instead of (Type -> Type) -> Type. I’m not sure exactly if there’s an added benefit to using this. I don’t immediately see a benefit to the extra type argument, except that Add can also be a Functor, which is nice.
type Expr f a = f (SProxy "expr") a
data Add f a = Add (Expr f a) (Expr f a)
derive instance functorAdd :: Functor (Add f)
instance hfunctorAdd :: HFunctor Add where hmap f (Add a b) = Add (hmap a) (hmap b)
But I’d be interested to see if this admits some neat stuff.