[Haskell-cafe] Computed promoted natural

[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