[Haskell-cafe] Developing Programs and Proofs Spontaneously using GADT

[Derek Elkins]

On Sat, 2007-08-04 at 23:25 +0800, Shin-Cheng Mu wrote:
> 
[...]
> In Haskell, the existential quantifier is mimicked by forall.
> We define:
> 
>  > data DepSum a p = forall i . DepSum (a i) (p i)
> 
> The term "dependent sum" is borrowed from the Omega tutorial
> of Sheard, Hook, and Linger [2] (why is it called a sum,
> not a product?).

There is already a dependent product.  One compelling reason for this
naming comes from category theory and how they relate to each other (the
dependent sum is a left adjoint, the dependent product is a right
adjoint [not directly to each other].)  They are related in the same way
products and sums are related, or universal quantification and
existential quantification are.  So, looking at the product case
(A,B)=AxB (and ()=1) and the sum case Either A B = A+B we can see how
they generalize to be the above.

Let's say we have a pair of the same type.  We can clearly represent it
as AxA, but another alternative is 1+1->A.  We can write the isomorphism
in Haskell:
pToF :: (a,a) -> (Either () () -> a)
pToF (x,_) (Left  ()) = x
pToF (_,y) (Right ()) = y

fToP :: (Either () () -> a) -> (a,a)
fToP f = (f (Left ()), f (Right ()))

Similarly for sums, A+A can be written (1+1)xA.  Again, the Haskell:
sToP :: Either a a -> (Either () (),a)
sToP (Left  x) = (Left  (), x)
sToP (Right x) = (Right (), x)

pToS :: (Either () (), a) -> Either a a
pToS (Left  (), x) = Left x
pToS (Right (), x) = Right x

Incidentally, this is how sums are usually encoded, i.e. a pair of a tag
and a value.  (Also incidentally, these are almost exactly the
isomorphisms defining adjunctions related to the ones that define
product and sum, i.e. the above definitions immediately fall out of the
category theory.)

So how to represent AxB or A+B with this encoding?  You can't.  However,
in a dependently typed language we can write (in some dependently typed
pseudo-Haskell) [for concreteness, let's set A=Int, B=String]:
f :: Either () () -> Type
f (Left  ()) = Int
f (Right ()) = String

Now we use the same definitions as above only with the types,
pToF :: (Int,String) -> (s :: Either () () -> f s)
fToP :: (s :: Either () () -> f s) -> (Int,String)
sToP :: Either Int String -> s :: Either () (). f s
pToS :: (s :: Either () (). f s) -> Either Int String

This leads to the dependent product being a function space when there is
no dependency, and similarly the dependent sum being a (normal) product.