Generating random type-level naturals

[wren ng thornton]

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