Here is the code where I'm having an issue:
{-# LANGUAGE GADTs, LANGUAGE DataKinds #-}
-- * Universe of Terms * --
type Id = String
data Term a where
Var :: Id -> Term a
Lam :: Id -> Type -> Term b -> Term (a :-> b)
App :: Term (a :-> b) -> Term a -> Term b
Let :: Id -> Term a -> Term b -> Term b
Tup :: Term a -> Term b -> Term (a :*: b) -- * existing tuple
Lft :: Term a -> Term (a :+: b) -- * existing sum
Rgt :: Term b -> Term (a :+: b)
Tru :: Term Boolean
Fls :: Term Boolean
Bot :: Term Unit
-- * Universe of Types * --
data Type = Type :-> Type | Type :*: Type | Type :+: Type | Boolean | Unit
So I want to extend Tup
to be defined over arbitrarily many arguments, same with sum. But a formulation involving lists would constrain the the final Term to one type of a:
Sum :: [Term a] -> Term a
I could just get rid of the a
and do something like:
Sum :: [Term] -> Term
But then I lose the very things I'm trying to express.
So how do I express some polymorphic Term without loss of expressiveness?
Doing this for a "list" is tricky using Haskell's type system, but can be done. As a starting point, it's easy enough if you restrict yourself to binary products and sums (and personally, I'd just stick with this):
To build an arbitrary-length sum type, we need an environment of terms. That's a heterogeneous list indexed by the types of the terms in it:
We then use a type family to collapse a list of types into a binary product type. Alternatively, we could add something like
Product [Type]
to theType
universe.The
prod
functions collapses such an environment to applications ofTup
. Again, you could also addProd
as a constructor of this type to theTerm
datatype.Arbitrary-length sums only take a single element to inject, but need a tag to indicate into which type of the sum to inject it:
Again, we have a type family and a function to build such a beast:
Of course, lots of variations or generalizations are possible, but this should give you an idea.