[Haskell-cafe] Type-Level Programming

[C. McCann]

On Sat, Jun 26, 2010 at 3:27 AM, Jason Dagit <dagit at codersbase.com> wrote:
> The types can depend on values.  For example, have you ever notice we have
> families of functions in Haskell like zip, zip3, zip4, ..., and liftM,
> liftM2, ...?
> Each of them has a type that fits into a pattern, mainly the arity
> increases.  Now imagine if you could pass a natural number to them and have
> the type change based on that instead of making new versions and
> incrementing the name.  That of course, is only the tip of the iceberg.

That's also a degenerate example, because it doesn't actually require
dependent types. What you have here are types dependent on *numbers*,
not *values* specifically. That type numbers are rarely built into
non-dependently-typed languages is another matter; encoding numbers
(inefficiently) as types is mind-numbingly simple in Haskell, not
requiring even any exciting GHC extensions (although encoding
arithmetic on those numbers will soon pile the extensions on).

Furthermore, families of functions of the flavor you describe are
doubly degenerate examples: The simplest encoding for type numbers are
the good old Peano numerals, expressed as nested type constructors
like Z, S Z, S (S Z), and so on... but the arity of a function is
*already* expressed as nested type constructors like [b] -> ([a] ->
[(b, a)]), [c] -> ([b] -> ([a] ->[(c,b, a)])), and such! The only
complication here is that the "zero" type changes for each number[0],
but in a very practical sense these functions already encode type
numbers.

Many alleged uses for dependent types are similarly trivial--using
them only as a shortcut for doing term-like computations on types.
With sufficient sweat, tears, and GHC extensions, most if not all of
said degenerate examples can be encoded directly at the type level.

For those following along at home, here's a quick cheat-sheet on
playing with type programs in GHC:
- Type constructors build new type "values"
- Type classes in general associate types with term values inhabiting them
- Type families and MPTCs with fundeps provide functions on types
- When an instance is selected, everything in its context is "evaluated"
- Instance selection that depends on the result of another type
function provides a sort of lazy evaluation (useful for control
structures)
- Getting anything interesting done usually needs UndecidableInstances
plus Oleg's TypeEq and TypeCast classes

Standard polymorphism also involves functions on types in a sense, but
doesn't allow computation on them. As a crude analogy, one could think
of type classes as allowing "pattern matching" on types, whereas
parametric polymorphism can only bind types to generic variables
without inspecting constructors.

>  Haskell's type system is sufficiently expressive that we can encode many
> instances of dependent types by doing some extra work.

Encoding *actual* instances of dependent types in some fashion is
indeed possible, but it's a bit trickier. The examples you cite deal
largely with making the  degenerate cases more pleasant to work with;
the paper by a charming bit of Church-ish encoding that weaves the
desired number-indexed function right into the definition of the zero
and successor, and she... well, she's a sight to behold to be sure,
but at the end of the day she's not really doing all that much either.

Since any value knowable at compile-time can be lifted to the type
level one way or another, non-trivial faux-dependent types must depend
on values not known until run-time--which of course means that the
exact type will be unknown until run-time as well, i.e., an
existential type. For instance, Oleg's uses of existential types to
provide static guarantees about some property of run-time values[1]
can usually be reinterpreted as a rather roundabout way of replicating
something most naturally expressed by actual dependent types.

Which isn't to say that type-level programming isn't useful, of
course--just that if you know the actual type at compile-time, you
don't really need dependent types.

- C.

[0] This is largely because of how Haskell handles tuples--the result
of a zipN function is actually another type number, not a zero, but
there's no simple way to find the successor of a tuple. More sensible,
from a number types perspective, would be to construct tuples using ()
as zero and (_, n) as successor. This would give us zip0 :: [()], zip1
:: [a] -> [(a, ())], zip2 :: [b] -> ([a] -> [(b, (a, ()))]), and so
on. The liftM and zipWith functions avoid this issue.
[1] See http://okmij.org/ftp/Haskell/types.html#branding and
http://okmij.org/ftp/Haskell/regions.html for instance.