[Haskell-cafe] Computed promoted natural

[Arie Peterson]

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