Generating random type-level naturals

Nicolas Frisby nicolas.frisby at gmail.com
Fri Nov 16 18:33:10 CET 2012


When wren's email moved this thread to the top of my inbox, I noticed that
I never sent this draft I wrote. It gives some concrete code along the line
of Wren's suggestion.

-----

The included code uses a little of this (singleton types) and a little of
that (implicit configurations).

  http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf

  http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf

As is so often the case with Haskell discussions, I'm not sure if this is
overkill for your actual needs. There might be simpler possible
solutions, but this idea at least matches my rather literal interpretation
of your email.

Also, I apologize if this approach is what you meant by "(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.)"

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE Rank2Types #-}

> module STandIC where

A data type for naturals; I'm assuming you have something like a useful
Arbitrary instance for these.

> data Nat = Z | S Nat

The corresponding singleton type.

> data Nat1 :: Nat -> * where
>   Z1 :: Nat1 Z
>   S1 :: Nat1 n -> Nat1 (S n)

Reification of a Nat; cf implicit configurations (ie prepose.pdf).

> reifyNat :: Nat -> (forall n. Nat1 n -> a) -> a
> reifyNat Z k = k Z1
> reifyNat (S n) k = reifyNat n $ k . S1

Here's my questionable assumption:

  If the code you want to use arbitrary type-level naturals with
  works for all type-level naturals, then it should be possible to
  wrap it in a function that fits as the second argument to reifyNat.

That may be tricky to do. I'm not sure it's necessarily always possible in
general; hence "questionable assumption". But maybe it'll work for you.

HTH. And I apologize if it's overkill; as Pedro was suggesting, there might
be simpler ways.



On Fri, Nov 16, 2012 at 12:52 AM, wren ng thornton <wren at freegeek.org>wrote:

> 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<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<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 at haskell.**org <Glasgow-haskell-users at haskell.org>
> http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-users<http://www.haskell.org/mailman/listinfo/glasgow-haskell-users>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121116/80916dfd/attachment.htm>


More information about the Glasgow-haskell-users mailing list