On 11/5/12 6:23 PM, Eric M. Pashman wrote:
I've been playing around with the idea of writing a genetic programming
implementation based on the ideas behind HList. Using type-level programming,
it's fairly straighforward to put together a program representation that's
strongly typed, that supports polymorphism, and that permits only well-typed
programs by construction. This has obvious advantages over vanilla GP
implementations. But it's impossible to generate arbitrary programs in such a
representation using standard Haskell.
Imagine that you have an HList-style heterogenous list of arbitrarily typed
Haskell values. It would be nice to be able to pull values from this collection
at random and use them to build up random programs. But that's not possible
because one can't write a function that outputs a value of arbitrary type. (Or,
more or less equivalently, one can't write dependently typed functions, and
trying to fake it at the type-level leads to the original problem.)
Actually, you can write functions with the necessary "dependent" types
using an old trick from Chung-chieh Shan and Oleg Kiselyov:
http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf
The first trick is to reify runtime values at the type level, which the
above paper explains how to do, namely: type class hackery.
The second trick is to overcome the issue you raised about not actually
having dependent types in Haskell. The answer to this is also given in
the paper, but I'll cut to the chase. The basic idea is that we just
need to be able to hide our dependent types from the compiler. That is,
we can't define:
reifyInt :: (n::Int) -> ...n...
but only because we're not allowed to see that pesky n. And the reason
we're not allowed to see it is that it must be some particular fixed
value only we don't know which one. But, if we can provide a function
eliminating n, and that function works for all n, then it doesn't matter
what the actual value is since we're capable of eliminating all of them:
reifyInt :: Int -> (forall n. ReflectNum n => n -> a) -> a
This is just the standard CPS trick we also use for dealing with
existentials and other pesky types we're not allowed to see. Edward
Kmett has a variation of this theme already on Hackage:
http://hackage.haskell.org/package/reflection
It doesn't include the implementation of type-level numbers, so you'll
want to look at the paper to get an idea about that, but the reflection
package does generalize to non-numeric types as well.
--
Live well,
~wren
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
