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 <[email protected]>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 <[email protected]>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@haskell.**org <[email protected]> >> http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-users<http://www.haskell.org/mailman/listinfo/glasgow-haskell-users> >> > > > _______________________________________________ > Glasgow-haskell-users mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
