How do you formulate n-ary product and sum types in this typed lambda calculus universe?

Question

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?

Answer 1

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):

{-# LANGUAGE GADTs, DataKinds, TypeOperators, KindSignatures, TypeFamilies #-} 

import Prelude hiding (sum) -- for later

-- * Universe of Terms * -- 

type Id = String 

data Term :: Type -> * 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) -- for binary products
   Lft :: Term a -> Term (a :+: b) -- new for sums
   Rgt :: Term b -> Term (a :+: b) -- new for sums
   Tru :: Term Boolean
   Fls :: Term Boolean
   Uni :: Term Unit -- renamed

-- * Universe of Types * --

data Type = Type :-> Type | Type :*: Type | Type :+: Type | Boolean | Unit | Void
  -- added :+: and Void for sums

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:

data Env :: [Type] -> * where
   Nil   :: Env '[]
   (:::) :: Term t -> Env ts -> Env (t ': ts)

infixr :::

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 the Type universe.

type family TypeProd (ts :: [Type]) :: Type
type instance TypeProd '[]       = Unit
type instance TypeProd (t ': ts) = t :*: TypeProd ts

The prod functions collapses such an environment to applications of Tup. Again, you could also add Prod as a constructor of this type to the Term datatype.

prod :: Env ts -> Term (TypeProd ts)
prod Nil        = Uni
prod (x ::: xs) = x `Tup` prod xs

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:

data Tag :: [Type] -> Type -> * where
   First :: Tag (t ': ts) t
   Next  :: Tag ts s -> Tag (t ': ts) s

Again, we have a type family and a function to build such a beast:

type family TypeSum (ts :: [Type]) :: Type
type instance TypeSum '[]       = Void
type instance TypeSum (t ': ts) = t :+: TypeSum ts

sum :: Tag ts t -> Term t -> Term (TypeSum ts)
sum First    x = Lft x
sum (Next t) x = Rgt (sum t x)

Of course, lots of variations or generalizations are possible, but this should give you an idea.