Brent Yorgey wrote:
As several people have pointed out, type-level programming in Haskell
resembles logic programming a la Prolog -- however, this actually only
applies to type-level programming using multi-parameter type classes
with functional dependencies [1] (which was until recently the only way to
do it).
Type-level programming using the newer type families [2] (which are
equivalent in power [3]) actually lets you program in a functional
style, much more akin to defining value-level functions in Haskell.
I did wonder what the heck a "type function" is or why you'd want one.
And then a while later I wrote some code along the lines of
class Collection c where
type Element c :: *
empty :: c -> Bool
first :: c -> Element c
So now it's like Element is a function that takes a collection type and
returns the type of its elements - a *type function*.
Suddenly the usual approach of doing something like
class Collection c where
empty :: c x -> Bool
first :: c x -> x
seems like a clumsy kludge, and the first snippet seems much nicer. (I
gather that GHC's implementation of all this is still "fragile" though?
Certainly I regularly get some very, very strange type errors if I try
to use this stuff...) The latter approach relies on "c" having a
particular kind, and the element type being a type argument (rather than
static), and in a specific argument position, and so on. So you can
construct a class that works for *one* type of element, or for *every*
type of element, but not for only *some*. The former approach (is that
type families or associated types or...? I get confused with all the
terms for nearly the same thing...) seems much cleaner to me. I never
liked FDs in the first place.
Not only is Element now a function, but you define it as a sort of
case-by-case pattern match:
instance Collection Bytestring where type Element ByteString = Word8
instance Collection [x] where type Element [x] = x
instance Ord x => Collection (Set x) where type Element (Set x) = x
...
So far, I haven't seen any other obvious places where this technology
might be useful (other than monads - which won't work). Then again, I
haven't looked particularly hard either. ;-)
However, all of this type-level programming is fairly *untyped*
Yeah, there is that.
-- the
only kinds available are * and (k1 -> k2)
Does # not count?
so type-level programming essentially takes place in the simply
typed lambda calculus with only a single base type, except you can't
write explicit lambdas.
Uh... if you say so? o_O
I'm currently working on a project with Simon Peyton-Jones, Dimitrios
Vytiniotis, Stephanie Weirich, and Steve Zdancewic on enabling *typed*
functional programming at the type level in GHC
Certainly sounds interesting...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
