type-level induction on Nat
Am 16.03.2014 09:40, schrieb Christiaan Baaij:
To answer the second question (under the assumption that you want phantom-type style Vectors and not GADT-style):
That works, someNatVal was the missing piece. Now the natural next question is how to perform type-level induction on Nat. This page mentions the Nat1 type, a unary representation of natural numbers: https://ghc.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats Since the unary natural number kind so ubiquituous in examples, is there a recommended module to import it from, which also contains the injectivity magic of FromNat1? I cannot see it in: http://hackage.haskell.org/package/base-4.7.0.0/candidate/docs/GHC-TypeLits.... although it seems to have been there: http://co-dan.github.io/base-docs/src/GHC-TypeLits.html
Am 16.03.2014 11:29, schrieb Henning Thielemann:
Since the unary natural number kind so ubiquituous in examples, is there a recommended module to import it from, which also contains the injectivity magic of FromNat1? I cannot see it in:
http://hackage.haskell.org/package/base-4.7.0.0/candidate/docs/GHC-TypeLits....
although it seems to have been there: http://co-dan.github.io/base-docs/src/GHC-TypeLits.html
Nat1 was removed here: https://github.com/ghc/packages-base/commit/5eaba365ff2354d3231f049866964d25... but commit message does not tell where it was moved. :-( Obviously it was not moved to "singletons".
On Mar 16, 2014, at 6:29 AM, Henning Thielemann wrote:
Since the unary natural number kind so ubiquituous in examples, is there a recommended module to import it from, which also contains the injectivity magic of FromNat1? I cannot see it in:
No. After some debate (on the libraries list, perhaps?), we decided to remove this from `base`, and I don't know of another library that has taken it on. If it were possible just to define a *kind* Nat1 with *type-level* conversions to and from Nat, we would have kept it in. But, we had to define a *type* Nat1 as well, and it only seemed sensible to have all the class instances, etc., to use this type in terms. This led to a fair amount of code, none of which was tightly coupled to code in `base`. There is a data-nat library, but it doesn't have the conversions to/from Nat built in. Richard
participants (2)
-
Henning Thielemann -
Richard Eisenberg