[prev in list] [next in list] [prev in thread] [next in thread]
List: haskell-cafe
Subject: Re: [Haskell-cafe] Type-Level Programming
From: Andrew Coppin <andrewcoppin () btinternet ! com>
Date: 2010-06-28 19:41:44
Message-ID: 4C28FAF8.2070603 () btinternet ! com
[Download RAW message or body]
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
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic