This is a more of a personal memo about dependent typing (and Haskell) than anything else. I expect to write more about this subject as I move forward to other similar subjects.

Dependent types

When we say that a term $b$ has a dependent type $B$, we are actually saying that its type depends on the value of another term $a$, i.e., $b: B_a$. Since the simplest case in which we can use a dependent type involves two terms, we talk about a dependent pair.

Dependent pair

A dependent pair can be informally understood as a pair of two terms $(a,b)$ where $a: A$ and $b: B_a$. This is also called a dependent sum because it captures the notion that the type is composed of an algebraic type sum:

The above notation is typically synthesized into $(a,b): \sum_{x:A} B_x$

One might try to emulate, in Haskell, such a dependent pair out of a Either (assume $A=$ Bool and $B_{True}=$ Int and $B_{False}=$ String):

data BoolPair = Either (Bool, Int) (Bool, String)

But this one does not rule out pairs such as Left (False, 3) which are exactly excluded by the dependent pair construction above.

Practical use

Why use a dependent pair? A part from more advanced uses such as proof construction, online tutorials cite dependent typing as a way to make programs more correct (e.g., avoiding access to zero sized vector). Others say that dependent types allow to describe more precisely the intended behavior of programs. The way I see it is that they can reduce the combinatorial space of cases to consider when building a function. For example,

f :: BoolPair -> ...

Since BoolPair is not a dependent pair, to write f you would have to consider, potentially, all combinations of the cartesian product $Bool \times (String + Int)$. Dependent pairs are effectively a tool to decrease this complexity and thus information overload.

How to build one

The first approach one can use to build a dependent pair is to follow the original definition using singletons. If one could enumerate all $a_i$ at the type level and produce a singleton type for each of them that would be enough¹. Lets consider again the above example.

A dependent pair such as BoolPair, i.e.,

could be encoded using GADTs, singletons and a type family:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

import Data.Singletons.Prelude

type family   B (x :: Bool)
type instance B 'True = Int
type instance B 'False = String

data BoolPair where
  (:*:) :: forall x. Sing x -> B x -> BoolPair

In practice:

• We use GADTs because they allow to define generic sum types and access each "addend" through pattern matching. The constructor of each pair is actually the :*: operator.
• x is special type variable; its kind is Bool and here we are using it to enumerate $A$, i.e., as a label that mimicks each inhabitant $a_i \in A$ for which we have to define a singleton.
• Sing x transforms each label $x$ into a singleton type $\{x\}$ for which one has to provide suitable value constructors (spoiler, the most important are already provided in the singletons library).
• B x transforms the same label through the type function $B(x)$ (here we use a type family to define it).

A possible usage that type-checks is the following:

f :: BoolPair -> String
f (STrue :*: n) = show n
f (SFalse :*: s) = s

while the following:

f' :: BoolPair -> String
f' (STrue :*: s) = s

would give a type-error, because the singleton value STrue requires an integer for the second value of the pair. What about a generic version of pairs that works with a generic t!=B and a generic s!='Bool? Look no further than the singletons library which has recently introduced sigma types:

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: Sing (fst :: s) -> t @@ fst -> Sigma s t

where the type constructor is :&: instead of :*:.

Existentials

Recall that a proposition can be seen as the collection (type) of all possible witnesses of its truth (propositions as types). In fact, the way witnesses are constructed by combining their types follows the way in which truth is combined through logic operators, provided that one can create a way to build such witnesses through an expression of a matching type ².

Let us now assume that

• $\{ a_i \}$ is the type of the witness that $a_i$ exists.
• $B_{a_i}$ is the type of the witnesses for a proposition that depends on $a_i$.

then the expression of the dependent pair:

can be interpreted in logic as

Which explains why dependent pairs are used to express existentially quantified predicates.