[Haskell-cafe] Computed promoted natural
Iavor Diatchki
iavor.diatchki at gmail.com
Thu Nov 8 18:34:21 CET 2012
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 <ariep at xs4all.nl> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121108/f186048c/attachment.htm>
More information about the Haskell-Cafe
mailing list