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.