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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
