8 Nov 16:54 2012

## Computed promoted natural

Arie Peterson <ariep <at> xs4all.nl>

2012-11-08 15:54:18 GMT

2012-11-08 15:54:18 GMT

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(Continue reading)/use/the computation, because it is not possible to create 'd :: Nat', at the type level, from the computed integer.