[Haskell-cafe] Computed promoted natural
ariep at xs4all.nl
Thu Nov 8 16:54:18 CET 2012
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
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,
More information about the Haskell-Cafe