Hello Arie,<div><br></div><div>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:</div>
<div><br></div><div><div><font face="courier new, monospace">{-# LANGUAGE DataKinds, KindSignatures, ExistentialQuantification #-}</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">import GHC.TypeLits</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data SomeNat = forall (n :: Nat). SomeNat (Sing n)</font></div><div><font face="courier new, monospace"><br></font></div><div>
<font face="courier new, monospace">getSomeNat :: IO SomeNat</font></div><div><font face="courier new, monospace">getSomeNat =</font></div><div><font face="courier new, monospace"> do x <- getLine</font></div><div><font face="courier new, monospace"> case reads x of</font></div>
<div><font face="courier new, monospace"> -- The use of `unsafeSingNat` is OK here because it is wrapped in `SomeNat`</font></div><div><font face="courier new, monospace"> -- so we are not assuming anything about the actual number.</font></div>
<div><font face="courier new, monospace"> [(n,_)] | n >= 0 -> return $ SomeNat $ unsafeSingNat n</font></div><div><font face="courier new, monospace"> _ -> putStrLn "Invalid number, try again." >> getSomeNat</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">main :: IO ()</font></div><div><font face="courier new, monospace">main =</font></div><div><font face="courier new, monospace"> do x <- getSomeNat</font></div>
<div><font face="courier new, monospace"> case x of</font></div><div><font face="courier new, monospace"> SomeNat s -> polyFun s s</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- The argument of this function are always going to be the same.</font></div>
<div><font face="courier new, monospace">-- (just an example, one could probably get more interesting properties)</font></div><div><font face="courier new, monospace">polyFun :: Sing (n :: Nat) -> Sing n -> IO ()</font></div>
<div><font face="courier new, monospace">polyFun x y = print (x,y)</font></div></div><div><br></div><div>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.</div>
<div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Nov 8, 2012 at 7:54 AM, Arie Peterson <span dir="ltr"><<a href="mailto:ariep@xs4all.nl" target="_blank">ariep@xs4all.nl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
<br>
I'm trying to use data kinds, and in particular promoted naturals, to simplify<br>
an existing program.<br>
<br>
The background is as follows: I have a big computation, that uses a certain<br>
natural number 'd' throughout, which is computed from the input. Previously,<br>
this number was present as a field in many of my data types, for instance<br>
<br>
> data OldA = OldA Integer …<br>
<br>
. There would be many values of this type (and others) floating around, with<br>
all the same value of 'd'. I would like to move this parameter to the type<br>
level, like this:<br>
<br>
> data NewA (d :: Nat) = NewA …<br>
<br>
The advantage would be, that the compiler can verify that the same value of<br>
'd' is used throughout the computation.<br>
<br>
Also, it would then be possible to make 'NewA' a full instance of 'Num',<br>
because 'fromInteger :: Integer -> NewA d' has a natural meaning (where the<br>
value of 'd' is provided by the type, i.e. the context in which the expression<br>
is used), while 'fromInteger :: Integer -> OldA' does not, because it is not<br>
possible to create the right value of 'd' out of thin air.<br>
<br>
<br>
Is this a sane idea? I seem to get stuck when trying to /use/ the computation,<br>
because it is not possible to create 'd :: Nat', at the type level, from the<br>
computed integer.<br>
<br>
Can one somehow instantiate the type variable 'd :: Nat' at an integer that is<br>
not statically known?<br>
<br>
Formulated this way, it sounds like this should not be possible, because all<br>
types are erased at compile time.<br>
<br>
However, it feels as though it might not be unreasonable in this situation,<br>
because the computation is polymorphic in the type 'd :: Nat'. I just want to<br>
substitute a specific value for 'd'.<br>
<br>
<br>
Maybe there is another way to approach this?<br>
<br>
<br>
Thanks for any advice,<br>
<br>
Arie<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>