On Sat, Jun 26, 2010 at 3:27 AM, Jason Dagit
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.