[Haskell-cafe] Computed promoted natural

[Arie Peterson]

Hello Iavor,


> One way to achieve the additional static checking is to use values of type
> `Sing (n :: Nat)` in the places where you've used `Integer` (and
> parameterize data structures by the `n`).  If the code is fully polymorphic
> in the `n`, then you can use it with values whose types as not statically
> know by using an existential.  Here is an example:
> […]
> I can elaborate more, just ask if this does not make sense.

Thanks for the example, it is very clear.

> One issue at
> the moment is that you have to pass the explicit `Sing` values everywhere,
> and it is a lot more convenient to use the `SingI` class in GHC.TypeLits.

Right. Apart from the inconvenience, it seems this approach doesn't allow the 
'Num' instance that I'm after: I can define a 'Num' instance for this type 
containing the 'Sing (n :: Nat)', but only when 'd' is an instance of 'SingI'.

> Unfortunately at the moment this only works for types that are statically
> known at compile time.  I think that we should be able to find a way to
> work around this, but we're not quite there yet.

OK. If there is progress in this area, I would be very interested!


Thanks and regards,

Arie