Generating random type-level naturals
wren ng thornton
wren at freegeek.org
Fri Nov 16 07:52:29 CET 2012
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:
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:
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.
More information about the Glasgow-haskell-users