[Haskell-cafe] Computed promoted natural
ariep at xs4all.nl
Fri Nov 9 17:01:09 CET 2012
> 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,
More information about the Haskell-Cafe