Eric M. Pashman | 6 Nov 00:23 2012
Picon

Generating random type-level naturals

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.)

One can, however, write a bit of Template Haskell to construct a random HNat. Something like,

    hNat 0 = [| hZero |]
    hNat n = [| hSucc $(hNat (n - 1)) |]

Call that with a random positive integer inside a splice and Template Haskell will give you a random HNat
that you can use to index an HList. There's your arbitrary Haskell value.

But this technique is of little practical value since it only works at compile-time. I've fiddled around
with the hint library, trying to interpret the Template Haskell to get random HNats at run-time. This
works, sort of, but there's no way to "liberate" the generated HNat because hint's `interpret` function
requires a type witness. A look-alike string from the `eval` function is as close as you can get.

Is there some dirty trick provided by the GHC API that would allow me to bind the generated HNat to a name and
pass it around in a way similar to what GHCi seems to do? I realize that I probably have a grossly optimistic
idea of what magic GHCi is performing when it interprets user input in a way that seems to allow this sort of thing.

To summarize, I'm basically trying to wrap up the following process programmatically:
(Continue reading)

José Pedro Magalhães | 6 Nov 14:17 2012
Picon

Re: Generating random type-level naturals

Hi Eric,

I'm not sure I fully understand what you want to do, so let me ask a basic question:
have you considered just using an Arbitrary instance of HsExpr? How would that
compare to what you are trying to achieve?


Cheers,
Pedro



On Mon, Nov 5, 2012 at 11:23 PM, Eric M. Pashman <eric.pashman <at> gmail.com> 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.)

One can, however, write a bit of Template Haskell to construct a random HNat. Something like,

    hNat 0 = [| hZero |]
    hNat n = [| hSucc $(hNat (n - 1)) |]

Call that with a random positive integer inside a splice and Template Haskell will give you a random HNat that you can use to index an HList. There's your arbitrary Haskell value.

But this technique is of little practical value since it only works at compile-time. I've fiddled around with the hint library, trying to interpret the Template Haskell to get random HNats at run-time. This works, sort of, but there's no way to "liberate" the generated HNat because hint's `interpret` function requires a type witness. A look-alike string from the `eval` function is as close as you can get.

Is there some dirty trick provided by the GHC API that would allow me to bind the generated HNat to a name and pass it around in a way similar to what GHCi seems to do? I realize that I probably have a grossly optimistic idea of what magic GHCi is performing when it interprets user input in a way that seems to allow this sort of thing.

To summarize, I'm basically trying to wrap up the following process programmatically:

    ghci> n <- randomInt       -- A random Int
    ghci> :load SomeModule.hs  -- Contains `hNat` as above
    ghci> let hn = $(hNat n)   -- Voila, a random HNat
    ghci> ...                  -- Do stuff with `hn`, then repeat

Is something along the lines of what I'm imagining possible? If not, can I get close enough for my purposes?

General insights and commentary are welcome as well.

Regards,

Eric


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
wren ng thornton | 16 Nov 07:52 2012

Re: Generating random type-level naturals

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
Nicolas Frisby | 16 Nov 18:33 2012
Picon

Re: Generating random type-level naturals

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).



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

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 16 Nov 21:08 2012
Picon

Re: Generating random type-level naturals

In  https://github.com/ekmett/rounded/blob/master/src/Numeric/Rounded/Precision.hs I borrow GHC's type level naturals for use directly as the reflection of a number of bits of precision.

That lets you work with `Rounded TowardZero Double` for the type of a number that offers 53 bits of mantissa and a known rounding mode or `Rounded TowardZero 512` to get a number with 512 bits of mantissa or you can use

reifyPrecision :: Int -> (forall (p :: *). Precision p => Proxy p -> a) -> a

to constructo a type p that you can use for `Rounded TowardZero p`.

This is how I piggyback on GHC's type-nats support. It'll get nicer once the actual solver is available and you can compute meaningfully with type level naturals.

-Edward

On Fri, Nov 16, 2012 at 12:33 PM, Nicolas Frisby <nicolas.frisby <at> gmail.com> wrote:
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).



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

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Eric M. Pashman | 17 Nov 18:12 2012
Picon

Re: Generating random type-level naturals

Wren, Nicolas, Edward, I'm grateful for your input. I'll sit down soon to take a closer look at your suggestions and code, and at the papers you've recommended.

My thanks,

Eric

On Nov 16, 2012, at 15:08 , Edward Kmett <ekmett <at> gmail.com> wrote:

In  https://github.com/ekmett/rounded/blob/master/src/Numeric/Rounded/Precision.hs I borrow GHC's type level naturals for use directly as the reflection of a number of bits of precision.

That lets you work with `Rounded TowardZero Double` for the type of a number that offers 53 bits of mantissa and a known rounding mode or `Rounded TowardZero 512` to get a number with 512 bits of mantissa or you can use

reifyPrecision :: Int -> (forall (p :: *). Precision p => Proxy p -> a) -> a

to constructo a type p that you can use for `Rounded TowardZero p`.

This is how I piggyback on GHC's type-nats support. It'll get nicer once the actual solver is available and you can compute meaningfully with type level naturals.

-Edward

On Fri, Nov 16, 2012 at 12:33 PM, Nicolas Frisby <nicolas.frisby <at> gmail.com> wrote:
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).



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

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane