Generating random type-level naturals

[Edward Kmett]

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.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).
>
>   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>
>>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> 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/0f1262cf/attachment-0001.htm>