Hello Arie,
One way to achieve the additional static checking is to use values of type
`Sing (n :: Nat)` in the places where you've used `Integer` (and
parameterize data structures by the `n`). If the code is fully polymorphic
in the `n`, then you can use it with values whose types as not statically
know by using an existential. Here is an example:
{-# LANGUAGE DataKinds, KindSignatures, ExistentialQuantification #-}
import GHC.TypeLits
data SomeNat = forall (n :: Nat). SomeNat (Sing n)
getSomeNat :: IO SomeNat
getSomeNat =
do x <- getLine
case reads x of
-- The use of `unsafeSingNat` is OK here because it is wrapped in
`SomeNat`
-- so we are not assuming anything about the actual number.
[(n,_)] | n >= 0 -> return $ SomeNat $ unsafeSingNat n
_ -> putStrLn "Invalid number, try again." >> getSomeNat
main :: IO ()
main =
do x <- getSomeNat
case x of
SomeNat s -> polyFun s s
-- The argument of this function are always going to be the same.
-- (just an example, one could probably get more interesting properties)
polyFun :: Sing (n :: Nat) -> Sing n -> IO ()
polyFun x y = print (x,y)
I can elaborate more, just ask if this does not make sense. One issue at
the moment is that you have to pass the explicit `Sing` values everywhere,
and it is a lot more convenient to use the `SingI` class in GHC.TypeLits.
Unfortunately at the moment this only works for types that are statically
known at compile time. I think that we should be able to find a way to
work around this, but we're not quite there yet.
-Iavor
On Thu, Nov 8, 2012 at 7:54 AM, Arie Peterson
Hi,
I'm trying to use data kinds, and in particular promoted naturals, to simplify an existing program.
The background is as follows: I have a big computation, that uses a certain natural number 'd' throughout, which is computed from the input. Previously, this number was present as a field in many of my data types, for instance
data OldA = OldA Integer …
. There would be many values of this type (and others) floating around, with all the same value of 'd'. I would like to move this parameter to the type level, like this:
data NewA (d :: Nat) = NewA …
The advantage would be, that the compiler can verify that the same value of 'd' is used throughout the computation.
Also, it would then be possible to make 'NewA' a full instance of 'Num', because 'fromInteger :: Integer -> NewA d' has a natural meaning (where the value of 'd' is provided by the type, i.e. the context in which the expression is used), while 'fromInteger :: Integer -> OldA' does not, because it is not possible to create the right value of 'd' out of thin air.
Is this a sane idea? I seem to get stuck when trying to /use/ the computation, because it is not possible to create 'd :: Nat', at the type level, from the computed integer.
Can one somehow instantiate the type variable 'd :: Nat' at an integer that is not statically known?
Formulated this way, it sounds like this should not be possible, because all types are erased at compile time.
However, it feels as though it might not be unreasonable in this situation, because the computation is polymorphic in the type 'd :: Nat'. I just want to substitute a specific value for 'd'.
Maybe there is another way to approach this?
Thanks for any advice,
Arie
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe