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?

Jeannettajeannette

This looks suspiciously like you want to sum Terms of different types, but the title of the question suggests you want to form a sum type. So what are you actually trying to do? – Chimney

Why not just use binary sums and products? Your Tup is already forming a product type. Similarly, you could have Lft :: Term a -> Term (a :+: b) and Rgt :: Term b -> Term (a :+: b) for a binary sum type. And add Type :+: Type to your universe of types, of course. – Wetmore

What @Wetmore said, and add Unt :: Term Unit if you want a unit for your product. – Landscapist

@Wetmore I wanted to generalize the Tup to one of arbitrarily many arguments, and similarly a Sum that's not restricted to two arguments – Jeannettajeannette

@Wetmore I updated the title to better reflect my question – Jeannettajeannette

@chibro2 but right now you need witnesses of both types to construct a Sum; this is not how it is usually defined. Usually Sum requires a witness of either of the types. Hence the need for Lft and Rgt in kosmikus solution – Inclement

@SassaNF ahh thank you. I was not aware of such subtleties but thanks for pointing it out! – Jeannettajeannette

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.

Wetmore