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

  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

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