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 ekm...@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.fri...@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).
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 w...@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
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).
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 w...@freegeek.orgwrote:
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.pdfhttp://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/reflectionhttp://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 Glasgow-haskell-users@haskell.org
http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing
Re: Generating random type-level naturals
In
https://github.com/ekmett/rounded/blob/master/src/Numeric/Rounded/Precision.hsI
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.fri...@gmail.comwrote:
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 w...@freegeek.orgwrote:
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.pdfhttp://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
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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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.pash...@gmail.comwrote: 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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
