Recently I needed to define a class with a restricted set of instances.
After some failed attempts I looked into the DataKinds extension and in
Giving Haskell a Promotion I found the example of a new kind Nat for
type level peano numbers. However the interesting part of a complete case
Hello Henning,
That's a way of branching on type-level data that I haven't seen yet. I don't
know of a name for it. However, if you find yourself needing to branch on
type-level data, I encourage you to check out singleton types:
data Nat = Zero | Succ Nat -- this will be promoted
data SNat
It seems very similar to Ryan Ingram's post a few years back
(pre-TypeNats):
http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html
The main difference is that he introduces the knowledge about zero vs.
suc as a constraint, and you introduce it as a parameter. In fact, his
induction
On Tue, 2 Apr 2013, Daniel Peebles wrote:
It seems very similar to Ryan Ingram's post a few years back
(pre-TypeNats):
http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html
The main difference is that he introduces the knowledge about zero vs. suc as
a constraint, and you
Henning Thielemann wrote:
However the interesting part of a complete case analysis on type level
peano numbers was only sketched in section 8.4 Closed type
families. Thus I tried again and finally found a solution that works
with existing GHC extensions:
You might like the following message
