Generating random type-level naturals

Edward Kmett ekmett at
Fri Nov 16 21:08:22 CET 2012

borrow GHC's type level naturals for use directly as the reflection of
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.


On Fri, Nov 16, 2012 at 12:33 PM, Nicolas Frisby
<nicolas.frisby at>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>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:
>> 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:
>> 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>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list