[Haskell-cafe] Computed promoted natural

[Iavor Diatchki]

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>