Computed promoted natural
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
Arie Peterson
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.
This is a known and nice way to do it, and not just possible, but actually quite beautiful. It all revolves around two related concepts called reflection and reification, the latter allowing precisely what you think is impossible: {-# RankNTypes, ScopedTypeVariables #-} reflectNum :: (Num a, ReflectNum n) => proxy n -> a reifyNum :: (Num a) => a -> (forall n. (ReflectNum n) => Proxy n -> b) -> b
Can one somehow instantiate the type variable 'd :: Nat' at an integer that is not statically known?
The idea is that reifyNum takes a polymorphic (!) function in 'n', such that the function can guarantee that it can handle any 'n', as long as it's an instance of ReflectNum. Now since the argument function is polymorphic, the reifyNum function itself can choose the type based on whatever value you pass as the first argument: reifyNum 0 k = k (Proxy :: Proxy Z) reifyNum n k = reifyNum (n - 1) (\(_ :: Proxy n) -> k (Proxy :: Proxy (S n))) Reflection and reification together are part of a larger concept called implicit configurations, and there is a paper about it.
Formulated this way, it sounds like this should not be possible, because all types are erased at compile time.
The types are, but the type class dictionaries remain. Of course there is no reason to reinvent the wheel here. Check out the 'reflection' library, which even uses some magic to make this as efficient as just passing the value right away (without Peano-constructing it). Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad.
On Thursday 08 November 2012 17:15:49 Ertugrul Söylemez wrote: | […] | The idea is that reifyNum takes a polymorphic (!) function in 'n', such | that the function can guarantee that it can handle any 'n', as long as | it's an instance of ReflectNum. Now since the argument function is | polymorphic, the reifyNum function itself can choose the type based on | whatever value you pass as the first argument: OK. It's nice that this is possible. The polymorphism should logically suffice to do this, but I wasn't sure if one could express this in Haskell. | Of course there is no reason to reinvent the wheel here. Check out the | 'reflection' library, which even uses some magic to make this as | efficient as just passing the value right away (without | Peano-constructing it). Right. So, let's try to fit GHC's singleton types to the reflection library.
import Data.Proxy import Data.Reflection import GHC.TypeLits
instance (SingI d,SingE d Integer) => Reifies (Sing d) Integer where reflect (_ :: p (Sing d)) = fromSing (sing :: Sing d)
This works, by itself. However, when trying to apply 'Data.Reflection.reify', I cannot create a polymorphic argument function 'f' that is polymorphic enough. I need the 'SingI d' constraint in my 'f', while according to 'reify', the type of 'f' should be
forall s. Reifies s a => Proxy s -> r
With this type, there is not enough known about 's' (no connection to the singleton types); the only thing you can do is apply 'reflect', but this only gives you an integer, leading back to the original problem. So, what I seem to need is a reification function for GHC's singleton natural types. For example:
reify :: Integer -> (forall d. (SingI d) => c d) -> (forall d. (SingI d) => c d -> r) -> r
(Where the second argument creates some piece of data that depends on the value of 'd', and the third argument uses this data to compute a final answer.) Maybe there is a simpler or more fundamental reification function, but this one would work for my application. Is this 'reify' possible? Regards, Arie
Arie Peterson
Right. So, let's try to fit GHC's singleton types to the reflection library.
I'm not sure if you're supposed to use the reflection library that way. The idea is simply this: reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r You pass in a value, any value you like actually ('reify' is fully polymorphic in 'a'), and the continuation receives a proxy that contains a type that represents that value. You can then use the 'Reifies' class to recover the original value from the type 's'. This goes with almost no runtime cost. In particular you should not write Reifies instances yourself. Let's say you want to write a data type for modular arithmetic that encodes the modulus in its type: {-# LANGUAGE ScopedTypeVariables #-} import Data.Proxy import Data.Reflection import Text.Printf data Mod n a = Mod !a !a instance (Integral a) => Eq (Mod n a) where Mod n x == Mod _ y = mod (x - y) n == 0 instance (Integral a, Show a) => Show (Mod n a) where show (Mod n x) = printf "(%s mod %s)" (show (mod x n)) (show n) instance (Integral a, Reifies n a) => Num (Mod n a) where Mod n x + Mod _ y = Mod n (mod (x + y) n) Mod n x - Mod _ y = Mod n (mod (x - y) n) Mod n x * Mod _ y = Mod n (mod (x * y) n) negate (Mod n x) = Mod n (n - x) abs = id signum x@(Mod _ 0) = x signum (Mod n _) = Mod n 1 fromInteger x = Mod n (mod (fromInteger x) n) where n = reflect (Proxy :: Proxy n) Notice that for speed I'm also saving the modulus as a value in the data constructor 'Mod'. Reflection is only used in the 'fromInteger' function, where the Mod value is first constructed. Then you can use reification to lift a modulus into its corresponding type. This is a very flexible interface that can carry type-level moduli even through a large monadic action: withModulus :: forall a b. (Integral a) => a -> (forall n. (Reifies n a) => (a -> Mod n a) -> (Mod n a -> a) -> b) -> b withModulus n k = reify n $ \(_ :: Proxy n) -> k (\x -> Mod n (mod x n) :: Mod n a) (\(Mod _ x) -> x) Usage: withModulus 101 $ \to from -> from $ (to 3 + 4)^17 The following is a highly simplified interface if you don't need a monad or anything, but just want to perform modular arithmetic: withModulus' :: forall a. a -> (forall n. (Reifies n a) => Mod n a) -> a withModulus' n mx = reify n $ \(_ :: Proxy n) -> case mx :: Mod n a of Mod _ x -> x Usage: withModulus' 101 ((3 + 4)^17) Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad.
On Friday 09 November 2012 17:53:54 Ertugrul Söylemez wrote:
I'm not sure if you're supposed to use the reflection library that way. The idea is simply this:
reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r
You pass in a value, any value you like actually ('reify' is fully polymorphic in 'a'), and the continuation receives a proxy that contains a type that represents that value. You can then use the 'Reifies' class to recover the original value from the type 's'. This goes with almost no runtime cost.
In particular you should not write Reifies instances yourself. Let's say you want to write a data type for modular arithmetic that encodes the modulus in its type: […]
OK, thanks for the example. So, in this approach, we drop the type parameter 'd' of kind 'Nat', and instead work with an type variable of kind *. Thanks and regards, Arie
On Friday 09 November 2012 17:53:54 Ertugrul Söylemez wrote:
I'm not sure if you're supposed to use the reflection library that way. The idea is simply this: […]
All right, I switched to this method, and it workes like a charm. It is also more general than my attempt using data kinds, in the sense that it workes for any type of parameter, not just integers and strings. Thanks for the advice. Regards, Arie
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
Hello Iavor,
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: […] I can elaborate more, just ask if this does not make sense.
Thanks for the example, it is very clear.
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.
Right. Apart from the inconvenience, it seems this approach doesn't allow the 'Num' instance that I'm after: I can define a 'Num' instance for this type containing the 'Sing (n :: Nat)', but only when 'd' is an instance of 'SingI'.
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.
OK. If there is progress in this area, I would be very interested! Thanks and regards, Arie
participants (3)
-
Arie Peterson -
Ertugrul Söylemez -
Iavor Diatchki