hey Iavor,
I just tried out today's head on a slightly more interesting example, and i
hit the limits of the type nat solver,
http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1
it seems like something where the solver *should* work
On Mon, Oct 7, 2013 at 1:35 AM, Iavor Diatchki
Hi,
On Sun, Oct 6, 2013 at 4:36 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:
hrmm, Why don't we have a proper bijection?
lets assume we have ToPeano and a corresponding ToNat, as above,
couldn't we have something like
asPeano :: (b~ ToPeano a, a ~ ToNat b)=> Proxy a -> Proxy b
or a suitable type level representaion thereof?
I think it should be quite easy to define such a function, but I am afraid I don't fully understand how to use it...
or are you saying that in 7.8, i should be able to just efficiently work directly on the nat rep
and have
class Cl (n::Nat) where
instance CL 0 where
instance Cl n => Cl (n+1)
and essentially get peano for free?
> I am not sure if this would help with your specific task, but things like this work:
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-} import GHC.TypeLits import Data.Proxy
class C (n :: Nat) where txt :: Proxy n -> String
instance C 0 where txt _ = "0"
instance C (n - 1) => C n where txt x = "1 + " ++ txt (prev x)
prev :: Proxy x -> Proxy (x - 1) prev _ = Proxy
example = txt (Proxy :: Proxy 3)
*Main> example "1 + 1 + 1 + 0"
-Iavor PS: All of this is committed in HEAD, please try it out and let me know if we need to do any last minute changes before the upcoming release.