GHC: Ticket #4385: Type-level natural numbers
http://trac.haskell.org/trac/ghc/ticket/4385
<p>
Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).
</p>
<p>
Existing features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!
</p>
<p>
Indeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).
</p>
<p>
Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:
</p>
<ul><li>a standard implementation,
</li><li>a better notation,
</li><li>better error messages,
</li><li>a more efficient implementation,
</li><li>more complete support for numeric operations.
</li></ul><p>
I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:
</p>
<pre class="wiki">http://code.galois.com/darcs/ghc-type-naturals/
</pre>en-usGHChttp://trac.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://trac.haskell.org/trac/ghc/ticket/4385
Trac 1.2.2iglooSat, 13 Nov 2010 20:14:46 GMTmilestone set
http://trac.haskell.org/trac/ghc/ticket/4385#comment:1
http://trac.haskell.org/trac/ghc/ticket/4385#comment:1
<ul>
<li><strong>milestone</strong>
set to <em>7.2.1</em>
</li>
</ul>
TicketdiatchkiMon, 15 Nov 2010 18:55:16 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:2
http://trac.haskell.org/trac/ghc/ticket/4385#comment:2
<p>
The repos implementing this feature are now at this location:
</p>
<p>
<a class="ext-link" href="http://code.galois.com/darcs/type-naturals/"><span class="icon"></span>http://code.galois.com/darcs/type-naturals/</a>
</p>
<p>
A brief explanation of the implementation and how to use it as available here:
</p>
<p>
<a class="ext-link" href="https://github.com/yav/memory-arrays/wiki"><span class="icon"></span>https://github.com/yav/memory-arrays/wiki</a>
</p>
TicketsimonpjWed, 24 Nov 2010 11:40:19 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:3
http://trac.haskell.org/trac/ghc/ticket/4385#comment:3
<p>
Great stuff. Here are some design issues I'd like to discuss. Probably email and your wiki is the place to discuss. (We can't edit your wiki... I wonder if you might use the GHC Trac Wiki instead?). But laying out the points for discussion here seems good:
</p>
<ul><li>I really, really want to make operators into type <strong>constructors</strong> rather than (as at present) type <strong>variables</strong>. So that we can write a type <code>(a + b)</code> rather than <code>(a :+ b)</code>. See <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors"><span class="icon"></span>http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors</a>. Doing this is, I think, straightforward, but it still needs doing.
</li></ul><ul><li>I found <code>integerToNat</code> hard to grok. Could we use an existential instead?
<pre class="wiki">data DynNat where
DN :: forall (n::Nat). Nat n -> DynNat
integerToNat :: Integer -> DynNat
</pre>Of course it's equivalent, but still.
</li></ul><ul><li>We need to think systematically about syntax. You have
<ul><li>A kind <code>Nat</code>
</li><li>A type <code>Nat :: Nat -> *</code>.
</li><li>A type class <code>TypeNat</code>
</li></ul></li></ul><blockquote>
<p>
And that's without thinking about a type-level equivalent of the kind <code>Nat</code>. At the type level we have <code>2 :: Nat</code>. It's be much nicer if at the term level we also had <code>2 :: Nat</code> (via the Num type class). But then the singleton type would have to be something different, <code>Nat1</code>, or <code>SingleNat</code>, or <code>Single</code>...?
</p>
</blockquote>
<blockquote>
<p>
The SHE notation (<a class="ext-link" href="http://personal.cis.strath.ac.uk/~conor/pub/she/"><span class="icon"></span>http://personal.cis.strath.ac.uk/~conor/pub/she/</a>) uses the "braces of upward mobility" to promote values to types, and types to kinds. I wonder if we could use that somehow.
</p>
</blockquote>
TicketdiatchkiWed, 24 Nov 2010 21:44:34 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:4
http://trac.haskell.org/trac/ghc/ticket/4385#comment:4
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:3" title="Comment 3">simonpj</a>:
</p>
<blockquote class="citation">
<p>
I wonder if you might use the GHC Trac Wiki instead?.
</p>
</blockquote>
<p>
I moved the wiki pages to the GHC wiki: <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeNats"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/TypeNats</a>
</p>
<blockquote class="citation">
<ul><li>I really, really want to make operators into type <strong>constructors</strong> rather than (as at present) type <strong>variables</strong>. So that we can write a type <code>(a + b)</code> rather than <code>(a :+ b)</code>. See <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors"><span class="icon"></span>http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors</a>. Doing this is, I think, straightforward, but it still needs doing.
</li></ul></blockquote>
<p>
Agreed. In fact, I hacked this up on the plane ride back from ICFP, but Happy pointed out that it leads to an ambiguity in imports and exports. I described the issue and a potential solution in <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors#Issues"><span class="icon"></span>http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors#Issues</a>
</p>
TicketKhudyakovTue, 04 Jan 2011 13:57:33 GMTcc set
http://trac.haskell.org/trac/ghc/ticket/4385#comment:5
http://trac.haskell.org/trac/ghc/ticket/4385#comment:5
<ul>
<li><strong>cc</strong>
<em>alexey.skladnoy@…</em> added
</li>
</ul>
<p>
I want to point out that type level signed integer numbers could be useful too. One use which immediately springs into mind is attaching dimension to physical values. Negative powers appears there all the time e.g. speed ~ cm·s<sup>{-1}. It's natural to encode dimensions using integer numbers.
</sup></p>
<p>
This is not top priority item but I think it's good to keep such possibility in mind.
</p>
TicketadamgundryWed, 05 Jan 2011 12:20:53 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:6
http://trac.haskell.org/trac/ghc/ticket/4385#comment:6
<ul>
<li><strong>cc</strong>
<em>adam.gundry@…</em> added
</li>
</ul>
<p>
I have been doing some theoretical work on type inference for systems like this, and am interested to see how this extension progresses. It is definitely worth considering signed integers: if nothing else, solving equations tends to become easier. Of course, natural numbers can be recovered once you have inequalities, though it might make sense to have special support for such a common use case.
</p>
TicketdiatchkiMon, 10 Jan 2011 02:23:55 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:7
http://trac.haskell.org/trac/ghc/ticket/4385#comment:7
<p>
Replying to <a class="closed ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385" title="#4385: feature request: Type-level natural numbers (closed: fixed)">diatchki</a>:
The most recently merged version of the implementation is at:
</p>
<p>
<a class="ext-link" href="http://code.galois.com/darcs/type-naturals/09-Jan-2011/"><span class="icon"></span>http://code.galois.com/darcs/type-naturals/09-Jan-2011/</a>
</p>
<p>
The patches there are relative to GHC (and relevant libraries) as of 09-Jan-2011.
</p>
TicketsimonpjMon, 10 Jan 2011 13:48:01 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:8
http://trac.haskell.org/trac/ghc/ticket/4385#comment:8
<p>
Iavor: what's your plan for this? I'd like to have it in the HEAD, but we need to resolve the design issues first. Also I'm unsure about whether you are actively developing or whether you've moved on to other things.
</p>
<p>
Oh, one other thing that isn't clear to me is how all this fits in FC. If a Pressburger solver shows that (a*b = b*a), say how is that expressed as a FC proof term?
</p>
<p>
Simon
</p>
TicketdiatchkiMon, 10 Jan 2011 19:32:20 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:9
http://trac.haskell.org/trac/ghc/ticket/4385#comment:9
<p>
Hello,
</p>
<p>
I am certainly still working on it, and I think that it'd be great to merge it with HEAD. What would be the best way to work on the design issues---I feel that these ticket comments do not have enough space to discuss things properly. Perhaps I will make a page on the wiki where we (meaning whoever is interested in this feature) can list all the issues and see how to solve them best? I'll update the ticket when I get a chance to do this.
</p>
<p>
Briefly, my current status is:
</p>
<ul><li>I've added the syntactic change to treat all symbols as type constructors, and the associated change to the module system. In the process I noticed that GHC does not really use the precedence machinery for infix predicates (classes, ~). Adding support for this is on my <span class="wikiextras phrase todo">TODO</span> list, so that we can write things like <code>(a + b ~ c)</code>, rather then <code>((a + b) ~ c)</code>.
</li></ul><ul><li>I've implemented the numeric type literals, which are of a new kind (currently called) Nat. I've added a new form of type <code>LiteralTy TyLit</code>, where <code>TyLit</code> is a type for type-level literals. Currently, it has only numbers in it but later we could add other things too, if we deemed it useful.
</li></ul><ul><li>I've added a set of operations on the type numbers, currently: comparison <code>(<=)</code>, addition <code>(+)</code>, multiplication <code>(*)</code>, and exponentiation <code>(^)</code>. By using equality constraints, we also get their inverses: subtraction, division, logarithms, and roots. My solver is by no means complete although it seems to work for a number of practical examples. I am sure that we can continue to improve it for a long time though.
</li></ul><p>
The current implementation cheats on the proofs for the equalities and (<=) because it uses "unsafeCoercions". At first I had it generate proofs but then you mentioned that you were redoing the evidence mechanism based on Brent's work, and the proofs were getting quite large and difficult to read so I removed them. It would not be hard to re-add them but we should decide on the granularity of the primitive axioms (coercions) to use. The trade-off is basically RISC vs CISC, a smaller set of simpler axioms tends to result in larger proofs.
</p>
<p>
There is also an issue about what evidence to pass for (<=). (<=) is similar to (~) (and any other class with no methods) in that it does not really need any runtime evidence. I could not see how to adopt the (~) mechanism to account for (<=) so, currently, the evidence for (<=) is basically a hack (the run-time evidence calls error if it is ever evaluated). It might be nice if we had a unified way to treat things without evidence (e.g., by having a special form of argument that does not emit any run-time code) but I have not looked into how hard would be to do this. Can anyone think of a better way to do this?
</p>
<ul><li>In the support library, I made the <code>DynNat</code> change that Simon described above. This worked out really nice because this type is basically the type of natural numbers at the value level, so I added all the usual instances for it and called it <code>Natural</code>, which mirrors <code>Integer</code>.
</li></ul><p>
I think that that's all.
</p>
TicketsimonpjTue, 11 Jan 2011 22:51:00 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:10
http://trac.haskell.org/trac/ghc/ticket/4385#comment:10
<ul>
<li><strong>cc</strong>
<em>sweirich@…</em> <em>dimitris@…</em> <em>byorgey@…</em> <em>Conor.McBride@…</em> added
</li>
</ul>
<p>
Good! My suggestions for progress:
</p>
<ul><li>Keep an up-to-date (preferably wiki) description of the users-eye view of the system. You had this before, but it may need updating eg with <code>DynNat</code>.
</li><li>Keep a wiki page, as you suggest, summarising design issues.
</li></ul><p>
You already have these, I think, here <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeNats"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/TypeNats</a>, although the division between "user manual", "design issues", and "implemetation notes" isn't very clear. Especially important is to summarise open design and implementation issues.
</p>
<p>
Email discussion belongs on cvs-ghc, I guess?
</p>
<p>
Concerning evidence, as soon as I get the new typechecker settled down I'm going to work on the evidence part of FC. In particular, equality evidence is currently treated like types, and erased, in contrast to class evidence which is not erased and is passed at runtime. I have a plan to treat both uniformly, not <em>erasing</em> equality evidence, but rather treating it as a value like the "state token" of the state monad. That is, a value that can be passed around in zero bits. This will make everying much nicer and more uniform.
</p>
<p>
Still the question remains of what evidence terms FC should have for numerics.
</p>
<p>
Iavor, if you continue to drive this, I'll be responsive. I'm adding Stephanie, Brent, Conor, Dimitrios to the cc list.
</p>
<p>
Simon
</p>
TicketpumpkinMon, 24 Jan 2011 23:11:34 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:11
http://trac.haskell.org/trac/ghc/ticket/4385#comment:11
<ul>
<li><strong>cc</strong>
<em>pumpkingod@…</em> added
</li>
</ul>
TicketthoughtpoliceSat, 29 Jan 2011 21:37:18 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:12
http://trac.haskell.org/trac/ghc/ticket/4385#comment:12
<ul>
<li><strong>cc</strong>
<em>as@…</em> added
</li>
</ul>
TicketsplSun, 30 Jan 2011 18:18:11 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:13
http://trac.haskell.org/trac/ghc/ticket/4385#comment:13
<ul>
<li><strong>cc</strong>
<em>leather@…</em> added
</li>
</ul>
TicketdiatchkiMon, 31 Jan 2011 00:45:50 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:14
http://trac.haskell.org/trac/ghc/ticket/4385#comment:14
<p>
Hello,
since a few people have joined the ticket I thought I'd post an update. I have been updating the documentation of how things work, and some of the design/implementation issues that I know of. Take a look here:
</p>
<p>
<a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeNats"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/TypeNats</a>
</p>
<p>
If you have the time, please try out the current implementation and send me feedback, I usually try to keep things in a working state. To get the code:
</p>
<pre class="wiki">git clone git://code.galois.com/type-naturals/ghc.git
</pre><p>
There are two branches in there, my work is on branch "type-nats" (branch "master" tracks the standrad GHC development branch).
</p>
<p>
As usual, before starting a build you'd need to get the libraries used by GHC. My work also requires some extra changes to "base" and "template-haskell" which are available in these darcs repos:
</p>
<pre class="wiki">http://code.galois.com/darcs/type-naturals/09-Jan-2011/base
http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell
</pre><p>
Usually, I use <code>darcs-all</code> to get the libraries from <code>darcs.haskell.org</code>, and then something like this:
</p>
<pre class="wiki">pushd libraries/base
darcs pull http://code.galois.com/darcs/type-naturals/09-Jan-2011/base
popd
pushd libraries/template-haskell
darcs pull http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell
popd
</pre><p>
Type-level nats are enabled with extensions <code>TypeNaturals</code> (e.g., <code>-XTypeNaturals</code>, or pragma <code>LANGUAGE TypeNaturals</code>.
</p>
TicketpumpkinTue, 01 Feb 2011 14:58:20 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:15
http://trac.haskell.org/trac/ghc/ticket/4385#comment:15
<p>
I'm wondering what is planned regarding support for ad-hoc "proofs". Although the solver is looking awesome, the general case of automatically solving (quantified) statements about naturals with addition, multiplication (boo), and order is undecidable. If I (taking as an example the memory-arrays repository) had a complex index calculation that led to the automatic solver not being able to determine that my numbers unify, what can I do to convince it? Does unsafeCoerce do the right thing on naturals? Can I compose small fundamental principles of natural arithmetic that the solver does understand to build up a larger proof, as one might do in an actual proof language? If so, will the construction of the proof have a runtime cost, or can it all be cleverly erased at runtime?
</p>
<p>
I apologize if these questions are answered elsewhere, but I was unable to see anything much covering them.
</p>
<p>
I'm very excited by this development and look forward to tinkering with it as soon as I get some time, so thanks!
</p>
TicketdiatchkiThu, 03 Feb 2011 18:21:42 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:16
http://trac.haskell.org/trac/ghc/ticket/4385#comment:16
<p>
Hello,
</p>
<p>
For the moment, there is no support for ad-hoc proofs. The problem you describe might occur when GHC encounters a type signature but it cannot show that the context of the type signature is sufficient to justify the function's implementation. As you say, this may be because GHC does not know enough math. In this case, one would have to either change (or remove) the type signature, or change the implementation (and, if the inference seems obvious, then send an e-mail to the GHC list so that we can teach GHC some more math :-).
</p>
<p>
<code>unsafeCoerce</code> works as usual but I've never had to use it because, usually, there is something different one can do. For example, the array indexes that you mentioned use type-nats as a phantom type only, so the library could provide arbitrary coercion functions, including something based on manual evidence construction, but I have not really thought about that.
</p>
TicketpumpkinThu, 03 Feb 2011 18:38:50 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:17
http://trac.haskell.org/trac/ghc/ticket/4385#comment:17
<p>
The main application I'm thinking about is REPA right now, which uses a fairly complex type to describe the shape of multidimensional arrays. The type is, however, not fully representative of the actual shape of the array, because we don't have easy type-level naturals. There's also some confusing overlap between the type-level shape (which mostly encodes the number of dimensions of the array) and the value-level shape (which actually contains the dimensions).
</p>
<p>
Using your typenats and some fancy GADT trickery, the index computations could be made exact and proved correct at compile time, to avoid any kind of index checking at runtime, but the computation is non-trivial, and basically involves proving that if you have a list of dimensions and a list of indices, then the usual multidimensional flattening computation preserves the < length requirement for the flat underlying array. I was modeling REPA in Agda a while back and came up with this:
</p>
<pre class="wiki">data Shape : ℕ → Set where
Z : Shape 1
_∷_ : ∀ {n} → (ss : Shape n) → (s : ℕ) → Shape (suc s * n)
data Index : ∀ {n} → Shape n → Set where
Z : Index Z
_∷_ : ∀ {m} {sh : Shape m} {n} → (is : Index sh) → (i : Fin (suc n)) → Index (sh ∷ n)
flatten : ∀ {n} {sh : Shape n} → Index sh → Fin n
flatten = {- lots more stuff to prove that the flattening computation preseves the Fin -}
</pre><p>
Although this is dependently typed in Agda, it could be modeled in Haskell too using GADTs that refine the type index to a typenat multiplication. When I get the time to compile your repo, I'll try translating this to Haskell with typenats and see if it can spot the fairly complicated behavior that I need to prove manually in Agda. I'll be very happy if it can!
</p>
<p>
Anyway, it's an exciting development in GHC! Now you just have to fight off all the proof-freaks like me that it attracts :P
</p>
TicketadamgundryFri, 04 Feb 2011 10:47:30 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:18
http://trac.haskell.org/trac/ghc/ticket/4385#comment:18
<p>
Nice work! It's good to see some progress in this direction.
</p>
<p>
We should certainly think about how users can provide more information to the constraint solver, either as explicit proofs or perhaps hints about useful lemmas to guide the search process. I'm not convinced that changing or removing type signatures on the whim of the compiler is a good strategy. (Can we even infer types properly for these things?)
</p>
<p>
I have been experimenting with the version of 9th January (while I try to figure out how to check out and build a more up to date version), so apologies if the following is a bit out of date. Perhaps I'm missing something, but I can't make the following classic example work:
</p>
<pre class="wiki">data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n+1) a
(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)
</pre><p>
In the last line, the solver fails to deduce ((1 + (n1 + m)) ~ (n + m)) from the context (n ~ (n1 + 1)). One use of unsafeCoerce is enough to get it accepted, but I can't see how two modify the type signature to make this go through. My point is not so much that this example fails, as the solver could presumably be extended to make it work, but that in general such problems will occur.
</p>
<p>
My perspective is from working with dependent types and inductive families (GADTs). I think that a lot of the interest in type-level numbers comes from their use along with GADTs, as pumpkin's example indicates, so we need to figure out how the interaction between the two will work.
</p>
<p>
One final thought: at the moment there doesn't seem to be any way to pattern match on numbers, at least without using natToInteger and so discarding statically-known information. For example, the Applicative functor instance for vectors includes
</p>
<pre class="wiki">pure :: Nat n -> a -> Vec n a
</pre><p>
which makes a vector full of a single value. At the moment, the implementation by pattern-matching and recursion on the first argument doesn't seem to be possible in a type-safe way. One can add a unary representation of numbers indexed by their Nat values inside the <a class="wiki" href="http://trac.haskell.org/trac/ghc/wiki/TypeNats">TypeNats</a> module abstraction barrier, but this is a bit clunky and inefficient.
</p>
Ticketsjoerd_visscherFri, 04 Feb 2011 12:53:30 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:19
http://trac.haskell.org/trac/ghc/ticket/4385#comment:19
<ul>
<li><strong>cc</strong>
<em>sjoerd@…</em> added
</li>
</ul>
TickethesselinkFri, 04 Feb 2011 20:39:01 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:20
http://trac.haskell.org/trac/ghc/ticket/4385#comment:20
<ul>
<li><strong>cc</strong>
<em>hesselink@…</em> added
</li>
</ul>
TicketdiatchkiMon, 07 Feb 2011 19:15:01 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:21
http://trac.haskell.org/trac/ghc/ticket/4385#comment:21
<p>
Hello,
</p>
<p>
I added some support for associativity over the weekend, and now the (+++) example works (I've pushed the changes to the git repo).
</p>
<p>
On the pattern matching issue: I also thought that using the unary representation might be clunky, but I played around with it this weekend, and I kind of like it. It leads to fairly natural looking definitions of simple inductive functions, and I don't think that it is even that inefficient---the unary number is lazily generated so it essentially corresponds to a sequence of checks on the real integer. Here is the code I played around with:
<a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeNats/InductiveDefinitions"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/TypeNats/InductiveDefinitions</a>
We might even be able to add a "fold" to deforest the intermediate "Zero" and "Succ" constructors.
</p>
<p>
(Previously, I was thinking that we should use type classes to do this sort of thing, but GHC does not like type functions in instance heads, and also we'd had to let it know that (x + 1) does not overlap with 0, etc., so overall this seems more complex.)
</p>
<p>
Finally a general note :-) I also think that this sort of "fake dependent types" / GADT programs are neat and useful but I wouldn't want to raise expectations too much because we really are pushing at the edges of Haskell's type system here---these simple examples use a lot of machinery (qualified types, type functions, GADTs, polymorphic recursion).
</p>
<p>
Another useful technique is to use type-level naturals as "phantom" types to provide safe library wrappers to unsafe primitives. This is a sort of intermediate step between the current state of Haskell and the dependent type/GADT world because it provides safety to the users of the library but only as long as the library is written correctly (i.e., the types do not help the library writer, but they help the library user). Here is an example of the technique:
</p>
<pre class="wiki">newtype Vec (n :: Nat) a = Vec [a]
empty :: Vec 0 a
empty = Vec []
mapVec :: (a -> b) -> Vec n a -> Vec n b
mapVec f (Vec xs) = Vec (map f xs)
catVec :: Vec m a -> Vec n a -> Vec (m + n) a
catVec (Vec xs) (Vec ys) = Vec (xs ++ ys)
-- etc..
</pre><p>
Note that here the types express the library writer's intention, but they do not enforce the correctness of the implementation. The benefit is that there are no complicated constraints to solve. Of course, constraints will arise when we use the library, but as long as the use is at concrete types, then the constraints would be easy to solve.
</p>
TicketlerkokWed, 16 Feb 2011 21:06:49 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:22
http://trac.haskell.org/trac/ghc/ticket/4385#comment:22
<ul>
<li><strong>cc</strong>
<em>erkokl@…</em> added
</li>
</ul>
<p>
Let me briefly chime in an express great interest in this project. Iavor has been able to pull in the sbv package (<a class="ext-link" href="http://hackage.haskell.org/package/sbv"><span class="icon"></span>http://hackage.haskell.org/package/sbv</a>) and make it work with his type-naturals, and it looks much cleaner and usable. Great work, looking forward to the official release. (And sbv will be an early adapter of this feature as a non-trivial application of it.)
</p>
TicketjweijersThu, 17 Feb 2011 18:34:03 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:23
http://trac.haskell.org/trac/ghc/ticket/4385#comment:23
<ul>
<li><strong>cc</strong>
<em>jeroen.weijers@…</em> added
</li>
</ul>
TicketconalThu, 17 Feb 2011 19:35:04 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:24
http://trac.haskell.org/trac/ghc/ticket/4385#comment:24
<ul>
<li><strong>cc</strong>
<em>conal@…</em> added
</li>
</ul>
TicketbasvandijkThu, 17 Feb 2011 22:52:02 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:25
http://trac.haskell.org/trac/ghc/ticket/4385#comment:25
<ul>
<li><strong>cc</strong>
<em>v.dijk.bas@…</em> added
</li>
</ul>
TickethelgikrsFri, 18 Feb 2011 07:37:47 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:26
http://trac.haskell.org/trac/ghc/ticket/4385#comment:26
<ul>
<li><strong>cc</strong>
<em>helgikrs@…</em> added
</li>
</ul>
TicketnwnFri, 18 Feb 2011 07:46:53 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:27
http://trac.haskell.org/trac/ghc/ticket/4385#comment:27
<ul>
<li><strong>cc</strong>
<em>nonowarn@…</em> added
</li>
</ul>
TicketdjahandarieSat, 26 Feb 2011 20:56:14 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:28
http://trac.haskell.org/trac/ghc/ticket/4385#comment:28
<ul>
<li><strong>cc</strong>
<em>djahandarie@…</em> added
</li>
</ul>
TicketChristiaanBaaijMon, 28 Feb 2011 13:46:03 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:29
http://trac.haskell.org/trac/ghc/ticket/4385#comment:29
<ul>
<li><strong>cc</strong>
<em>christiaan.baaij@…</em> added
</li>
</ul>
TicketLemmingMon, 28 Feb 2011 16:31:54 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:30
http://trac.haskell.org/trac/ghc/ticket/4385#comment:30
<ul>
<li><strong>cc</strong>
<em>ghc@…</em> added
</li>
</ul>
<p>
The llvm package highly needs something that is faster than the type level arithmetic provided by type-level. Currently compiling llvm related code can require several seconds due to the involved vector size computations. I am still curious what comes next after type level naturals. :-)
</p>
TicketjeltschWed, 02 Mar 2011 21:14:50 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:31
http://trac.haskell.org/trac/ghc/ticket/4385#comment:31
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:3" title="Comment 3">simonpj</a>:
</p>
<blockquote class="citation">
<p>
I really, really want to make operators into type <strong>constructors</strong> rather than (as at present) type <strong>variables</strong>. So that we can write a type <code>(a + b)</code> rather than <code>(a :+ b)</code>. See <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors"><span class="icon"></span>http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors</a>. Doing this is, I think, straightforward, but it still needs doing.
</p>
</blockquote>
<p>
Really nice. What GHC version can be expected to have this feature? I’d like to use it.
</p>
TicketbjornbmThu, 10 Mar 2011 08:49:11 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:32
http://trac.haskell.org/trac/ghc/ticket/4385#comment:32
<ul>
<li><strong>cc</strong>
<em>bjornbm</em> added
</li>
</ul>
TicketillissiusThu, 17 Mar 2011 11:44:47 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:33
http://trac.haskell.org/trac/ghc/ticket/4385#comment:33
<ul>
<li><strong>cc</strong>
<em>illissius@…</em> added
</li>
</ul>
TicketFSaladSat, 16 Apr 2011 18:57:52 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:34
http://trac.haskell.org/trac/ghc/ticket/4385#comment:34
<ul>
<li><strong>cc</strong>
<em>danlex@…</em> added
</li>
</ul>
TicketPHOTue, 19 Apr 2011 13:41:43 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:35
http://trac.haskell.org/trac/ghc/ticket/4385#comment:35
<ul>
<li><strong>cc</strong>
<em>pho@…</em> added
</li>
</ul>
TicketdanknaSun, 22 May 2011 12:59:19 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:36
http://trac.haskell.org/trac/ghc/ticket/4385#comment:36
<ul>
<li><strong>cc</strong>
<em>dankna@…</em> added
</li>
</ul>
TicketFavoniaWed, 25 May 2011 04:26:44 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:37
http://trac.haskell.org/trac/ghc/ticket/4385#comment:37
<ul>
<li><strong>cc</strong>
<em>favonia@…</em> added
</li>
</ul>
TicketdanknaSat, 30 Jul 2011 07:23:41 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:38
http://trac.haskell.org/trac/ghc/ticket/4385#comment:38
<p>
So I've been playing around with this the past couple days. I have picked a different toy project than everybody else's; instead of sized arrays, I'm doing dimensioned quantities. So for example I want to be able to have types Quantity Kilo Watt Int and Quantity Mega Second Int and know that the product of them is Quantity Giga Joule Int. To do this I am having one type-level int (not nat) for each of the seven SI fundamental units length, time, etc, representing the power to which that unit is present. So velocity would have length to power 1 and time to power -1, and everything else to power 0. This unfortunately does not encompass currencies, but oh well.
</p>
<p>
So that would work, except as far as I can tell, the obvious way to define type-level integers in terms of type-level naturals isn't possible.
</p>
<p>
Here's what I'm doing:
</p>
<pre class="wiki">data IntType :: * -> Nat -> *
data Negative
data NonNegative
class IntClass int
instance IntClass (IntType NonNegative num)
instance (1 <= num) => IntClass (IntType Negative num)
</pre><p>
So far so good, except there's no way to write a type function PlusInt. I eventually realized that I could reduce it to writing MinusNat instead, which makes for a clearer explanation of why it isn't possible, so that's the example I'll give here:
</p>
<pre class="wiki">type family MinusNat a b
type instance MinusNat (ab ~ a + b) b = a
</pre><p>
or alternatively
</p>
<pre class="wiki">type family MinusNat a b
type instance (ab ~ a + b) => MinusNat ab b = a
</pre><p>
But of course neither is possible, because neither type-synonym instances nor type contexts can be used like that. I puzzled over why that was for a moment before people in #haskell pointed out to me that it would require GHC to read the number's mind, effectively.
</p>
<p>
Anyway, I can think of two ways to remedy this. The more invasive way would be to add a solver that can actually do that. The less invasive way would be to add a kind Int which is a superkind of Nat and has minus built-in. But I don't like that approach as much because it wouldn't let people implement division or logarithms.
</p>
<p>
I don't know what you refer to with the "evidence system" above, because I don't understand the internals of the typechecker. I'm willing to write some code to make this happen, but I need to discuss the design first. So I'm writing this post attached to the ticket so that everyone interested can respond. I may also direct people in #ghc to this tomorrow morning, but I don't know how much time they'll have to spare.
</p>
TicketjeltschSat, 30 Jul 2011 07:33:51 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:39
http://trac.haskell.org/trac/ghc/ticket/4385#comment:39
<p>
Would it be possible to name the new kind <code>Natural</code> instead of <code>Nat</code>? That way, the naming would be consistent with the naming of integer types, where <code>Int</code> only refers to a subset of the integers, while <code>Integer</code> refers to the complete set.
</p>
TicketjhenahanSun, 31 Jul 2011 07:32:11 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:40
http://trac.haskell.org/trac/ghc/ticket/4385#comment:40
<ul>
<li><strong>cc</strong>
<em>jhenahan@…</em> added
</li>
</ul>
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:39" title="Comment 39">jeltsch</a>:
</p>
<blockquote class="citation">
<p>
Would it be possible to name the new kind <code>Natural</code> instead of <code>Nat</code>? That way, the naming would be consistent with the naming of integer types, where <code>Int</code> only refers to a subset of the integers, while <code>Integer</code> refers to the complete set.
</p>
</blockquote>
<p>
Cf. Agda.
</p>
TicketjeltschSun, 31 Jul 2011 16:09:11 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:41
http://trac.haskell.org/trac/ghc/ticket/4385#comment:41
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:40" title="Comment 40">jhenahan</a>:
</p>
<blockquote class="citation">
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:39" title="Comment 39">jeltsch</a>:
</p>
<blockquote class="citation">
<p>
Would it be possible to name the new kind <code>Natural</code> instead of <code>Nat</code>? That way, the naming would be consistent with the naming of integer types, where <code>Int</code> only refers to a subset of the integers, while <code>Integer</code> refers to the complete set.
</p>
</blockquote>
<p>
Cf. Agda.
</p>
</blockquote>
<p>
Hmm, the type of natural numbers is called ℕ in Agda. Well, the module it’s defined in is called <code>Data.Nat</code>. But why should Haskell be consistent with Agda, but not consistent with itself?
</p>
Ticketsjoerd_visscherSun, 31 Jul 2011 18:40:41 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:42
http://trac.haskell.org/trac/ghc/ticket/4385#comment:42
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:38" title="Comment 38">dankna</a>:
</p>
<blockquote class="citation">
<p>
So that would work, except as far as I can tell, the obvious way to define type-level integers in terms of type-level naturals isn't possible.
</p>
</blockquote>
<p>
Have you tried defining type-level integer in terms of 2 type-level naturals, the value being the difference between the 2 naturals:
</p>
<pre class="wiki">data IntType :: Nat -> Nat -> *
type family Minus a b
type instance Minus (IntType a b) (IntType c d) = IntType (a + d) (b + c)
</pre><p>
The type for f.e. -2 would then be <code>forall n. IntType n (n + 2)</code>.
</p>
TicketdanknaSun, 31 Jul 2011 19:34:19 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:43
http://trac.haskell.org/trac/ghc/ticket/4385#comment:43
<p>
I haven't tried that, no, but I don't see how it could work - surely that loses the very nice property that type equality corresponds to numeric equality?
</p>
Ticketsjoerd_visscherTue, 02 Aug 2011 17:33:10 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:44
http://trac.haskell.org/trac/ghc/ticket/4385#comment:44
<p>
Instead of (i ~ IntType Negative 2) you get (i ~ IntType n (n + 2)).
</p>
TicketreinerpFri, 05 Aug 2011 07:34:43 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:45
http://trac.haskell.org/trac/ghc/ticket/4385#comment:45
<ul>
<li><strong>cc</strong>
<em>reiner.pope@…</em> added
</li>
</ul>
TicketacfoltzerWed, 17 Aug 2011 00:33:37 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:46
http://trac.haskell.org/trac/ghc/ticket/4385#comment:46
<ul>
<li><strong>cc</strong>
<em>acfoltzer@…</em> added
</li>
</ul>
TicketnathanhowellFri, 18 Nov 2011 22:47:03 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:47
http://trac.haskell.org/trac/ghc/ticket/4385#comment:47
<ul>
<li><strong>cc</strong>
<em>nathanhowell@…</em> added
</li>
</ul>
TicketbjornbmWed, 08 Feb 2012 03:03:43 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:48
http://trac.haskell.org/trac/ghc/ticket/4385#comment:48
<p>
It seems this ticket needs an update by someone in the know. I understand <a class="wiki" href="http://trac.haskell.org/trac/ghc/wiki/TypeNats">TypeNats</a> didn't make it into 7.4.1 in the end so at least the milestone is inaccurate(?). Can we still expect to see <a class="wiki" href="http://trac.haskell.org/trac/ghc/wiki/TypeNats">TypeNats</a> in GHC?
</p>
TicketdiatchkiThu, 09 Feb 2012 06:24:10 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:49
http://trac.haskell.org/trac/ghc/ticket/4385#comment:49
<p>
Hello,
</p>
<p>
work on the type nats is still in progress, support for type nat literlas, generalized type type-level operators, and type-level string literals is available in the type-nats branch of GHC.
</p>
<p>
There used to be a solver for type-level functions on nats as well, but it is dibaled for the moment. The current task is to decide how to integrate the evidence generated by the solver with the evidence that GHC uses. I've been a bit busy with work lately, but I am hoping to restart hacking on the solver integration in the next few weeks.
</p>
TicketiglooThu, 09 Feb 2012 15:00:01 GMTmilestone changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:50
http://trac.haskell.org/trac/ghc/ticket/4385#comment:50
<ul>
<li><strong>milestone</strong>
changed from <em>7.4.1</em> to <em>7.6.1</em>
</li>
</ul>
TicketgoldfireMon, 30 Jul 2012 13:33:11 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:51
http://trac.haskell.org/trac/ghc/ticket/4385#comment:51
<ul>
<li><strong>cc</strong>
<em>eir@…</em> added
</li>
</ul>
TicketdmccleanMon, 13 Aug 2012 22:02:59 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:52
http://trac.haskell.org/trac/ghc/ticket/4385#comment:52
<p>
I notice this is in the 7.6.1 RC without a constraint solver.
Is there a plan to implement the constraint solver for 7.6.1?
If not, it might make sense to delay implementing this at all until the solver can be implemented, to retain more flexibility for making any changes that might be informed by the solver work.
</p>
TicketdmccleanMon, 13 Aug 2012 22:04:03 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:53
http://trac.haskell.org/trac/ghc/ticket/4385#comment:53
<ul>
<li><strong>cc</strong>
<em>douglas.mcclean@…</em> added
</li>
</ul>
TicketcarterMon, 27 Aug 2012 21:26:28 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:54
http://trac.haskell.org/trac/ghc/ticket/4385#comment:54
<p>
wait.... theres no constraint solver in yet? that would explain why I had the bugs I reported wrt type nats last week!
</p>
TicketiglooWed, 12 Sep 2012 11:12:00 GMTmilestone changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:55
http://trac.haskell.org/trac/ghc/ticket/4385#comment:55
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.1</em> to <em>7.6.2</em>
</li>
</ul>
TickethvrFri, 16 Nov 2012 14:37:57 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:56
http://trac.haskell.org/trac/ghc/ticket/4385#comment:56
<ul>
<li><strong>cc</strong>
<em>hvr@…</em> added
</li>
</ul>
TicketpashThu, 31 Jan 2013 23:34:07 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:57
http://trac.haskell.org/trac/ghc/ticket/4385#comment:57
<ul>
<li><strong>cc</strong>
<em>eric.pashman@…</em> added
</li>
</ul>
TicketmaltemWed, 08 May 2013 10:39:24 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:58
http://trac.haskell.org/trac/ghc/ticket/4385#comment:58
<p>
I'm trying out the type-nats branch and the wiki says to complain when the solver cannot solve something, so here we go:
</p>
<pre class="wiki">Bug.hs:22:29:
Could not deduce ((2 * n) ~ ((2 * n1) + 2))
from the context (n ~ (n1 + 1))
</pre><p>
The code is attached. I'd welcome a hint how I can work around the error (the wiki mentions that this should typically be possible, but I don't understand how).
</p>
TicketmaltemWed, 08 May 2013 10:39:56 GMTattachment set
http://trac.haskell.org/trac/ghc/ticket/4385
http://trac.haskell.org/trac/ghc/ticket/4385
<ul>
<li><strong>attachment</strong>
set to <em>Ticket.hs</em>
</li>
</ul>
TicketdiatchkiWed, 08 May 2013 16:00:11 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:59
http://trac.haskell.org/trac/ghc/ticket/4385#comment:59
<p>
Thanks, I'll take a look and try to improve the solver. Unfortunately, I don't think that there's an easy way to work around this in the polymorphic case. If you could instantiate the <code>n</code>s somehow, it'd get solved, but I know that's not always an option.
</p>
TicketdarchonThu, 23 May 2013 15:44:56 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:60
http://trac.haskell.org/trac/ghc/ticket/4385#comment:60
<p>
I get a similar error implementing concat for vectors:
</p>
<pre class="wiki">data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
vappend :: Vec n a -> Vec m a -> Vec (n + m) a
vappend Nil ys = ys
vappend (x :> xs) ys = x :> (vappend xs ys)
vconcat :: Vec n (Vec m a) -> Vec (n * m) a
vconcat Nil = Nil
vconcat (x :> xs) = vappend x (vconcat xs)
</pre>
TicketArtyom.KazakTue, 18 Jun 2013 23:09:35 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:61
http://trac.haskell.org/trac/ghc/ticket/4385#comment:61
<ul>
<li><strong>cc</strong>
<em>Artyom.Kazak@…</em> added
</li>
</ul>
TicketguestFri, 28 Jun 2013 16:32:14 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:62
http://trac.haskell.org/trac/ghc/ticket/4385#comment:62
<p>
Is there a way to make the following work?
</p>
<pre class="wiki">Couldn't match type `1 + 0' with `1'
</pre><p>
Here is a test to reproduce this.
</p>
<p>
(test2 and test3 produce the errors when the line that don't work are uncommented) This is a file:
</p>
<pre class="wiki">--file: Scratch.hs {-# Language DataKinds?, KindSignatures?, TypeOperators? #-}
import GHC.TypeLits?
test1 = sing :: Sing (1) --works
--test2 = sing :: Sing (1+0) --doesn't
data F (n::Nat) = F ()
f :: F n -> F n -> () f _ _ = ()
x = F () :: F (1) --works
--x = F () :: F (1+0) --doesn't
y = F () :: F (1)
test3 = f x y
</pre>
Ticketnorm2782Tue, 30 Jul 2013 06:18:21 GMTcc changed; difficulty set
http://trac.haskell.org/trac/ghc/ticket/4385#comment:63
http://trac.haskell.org/trac/ghc/ticket/4385#comment:63
<ul>
<li><strong>cc</strong>
<em>j.stutterheim@…</em> added
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
TicketnschSat, 05 Oct 2013 11:54:34 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:64
http://trac.haskell.org/trac/ghc/ticket/4385#comment:64
<ul>
<li><strong>cc</strong>
<em>mail@…</em> added
</li>
</ul>
TicketghornWed, 09 Oct 2013 14:02:34 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:65
http://trac.haskell.org/trac/ghc/ticket/4385#comment:65
<ul>
<li><strong>cc</strong>
<em>gregmainland@…</em> added
</li>
</ul>
TicketLemmingTue, 11 Mar 2014 20:11:56 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:66
http://trac.haskell.org/trac/ghc/ticket/4385#comment:66
<p>
Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in
</p>
<blockquote>
<p>
<a href="http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/">http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/</a>
</p>
</blockquote>
TickethvrTue, 11 Mar 2014 22:14:11 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:67
http://trac.haskell.org/trac/ghc/ticket/4385#comment:67
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:66" title="Comment 66">Lemming</a>:
</p>
<blockquote class="citation">
<p>
Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in
</p>
<blockquote>
<p>
<a href="http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/">http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/</a>
</p>
</blockquote>
</blockquote>
<p>
does <a href="http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals">http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals</a> count?
</p>
TicketLemmingTue, 11 Mar 2014 22:27:47 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:68
http://trac.haskell.org/trac/ghc/ticket/4385#comment:68
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:67" title="Comment 67">hvr</a>:
</p>
<blockquote class="citation">
<p>
Replying to <a class="ticket" href="http://trac.haskell.org/trac/ghc/ticket/4385#comment:66" title="Comment 66">Lemming</a>:
</p>
<blockquote class="citation">
<p>
Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in
</p>
<blockquote>
<p>
<a href="http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/">http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/</a>
</p>
</blockquote>
</blockquote>
<p>
does <a href="http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals">http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals</a> count?
</p>
</blockquote>
<p>
Indeed, that's a nice start. What about type-level natural number operations and predicates? What about conversion from type-level numbers to data-level numbers? I found:
</p>
<blockquote>
<p>
<a class="ext-link" href="https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Basics"><span class="icon"></span>https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Basics</a>
<a class="ext-link" href="https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Operations"><span class="icon"></span>https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Operations</a>
</p>
</blockquote>
<p>
Do these articles reflect the current state of implementation?
</p>
<p>
I also found the announcement:
</p>
<blockquote>
<p>
<a class="ext-link" href="http://www.well-typed.com/blog/85"><span class="icon"></span>http://www.well-typed.com/blog/85</a>
</p>
</blockquote>
<p>
where many feature names are linked to the GHC documentation, but "type-level natural numbers" is not. I also like to see the keyword "type-level natural number" somewhere in GHC docs, since this is how this feature is advertised.
</p>
TicketthoughtpoliceMon, 14 Jul 2014 13:04:47 GMTmilestone changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:69
http://trac.haskell.org/trac/ghc/ticket/4385#comment:69
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.2</em> to <em>7.10.1</em>
</li>
</ul>
<p>
Moving to 7.10.1.
</p>
TicketthoughtpoliceTue, 23 Dec 2014 13:34:10 GMTmilestone changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:70
http://trac.haskell.org/trac/ghc/ticket/4385#comment:70
<ul>
<li><strong>milestone</strong>
changed from <em>7.10.1</em> to <em>7.12.1</em>
</li>
</ul>
<p>
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
</p>
TicketdmccleanThu, 19 Feb 2015 22:40:33 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:71
http://trac.haskell.org/trac/ghc/ticket/4385#comment:71
<p>
Could anyone provide an update on the current state of efforts to improve the constraint solver?
</p>
TicketadamgundryFri, 20 Feb 2015 07:55:00 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:72
http://trac.haskell.org/trac/ghc/ticket/4385#comment:72
<p>
Iavor can probably say more than me, but I believe he is currently working on a type-nats constraint solver as a typechecker plugin that communicates with an SMT solver: <a class="ext-link" href="https://github.com/yav/type-nat-solver"><span class="icon"></span>https://github.com/yav/type-nat-solver</a>
</p>
<p>
More generally, the aim of the typechecker plugins work is to make this sort of thing easier to experiment with.
</p>
TicketadamgundryFri, 20 Feb 2015 07:59:25 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:73
http://trac.haskell.org/trac/ghc/ticket/4385#comment:73
<ul>
<li><strong>cc</strong>
<em>adamgundry</em> added; <em>adam.gundry@…</em> removed
</li>
</ul>
TicketthoughtpoliceFri, 11 Sep 2015 08:38:26 GMTmilestone changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:74
http://trac.haskell.org/trac/ghc/ticket/4385#comment:74
<ul>
<li><strong>milestone</strong>
changed from <em>7.12.1</em> to <em>8.0.1</em>
</li>
</ul>
<p>
Milestone renamed
</p>
TicketWrenThorntonTue, 15 Sep 2015 10:17:40 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/4385#comment:75
http://trac.haskell.org/trac/ghc/ticket/4385#comment:75
<ul>
<li><strong>cc</strong>
<em>wren@…</em> added
</li>
</ul>
TicketthomieSun, 24 Jan 2016 18:07:53 GMTmilestone deleted
http://trac.haskell.org/trac/ghc/ticket/4385#comment:76
http://trac.haskell.org/trac/ghc/ticket/4385#comment:76
<ul>
<li><strong>milestone</strong>
<em>8.0.1</em> deleted
</li>
</ul>
TicketbgamariWed, 16 Aug 2017 00:03:28 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:77
http://trac.haskell.org/trac/ghc/ticket/4385#comment:77
<p>
Iavor, what is the status of your plugin? Given that it seems unlikely that we'll merge an SMT solver into GHC, perhaps we should close this?
</p>
TicketdiatchkiWed, 16 Aug 2017 18:09:09 GMT
http://trac.haskell.org/trac/ghc/ticket/4385#comment:78
http://trac.haskell.org/trac/ghc/ticket/4385#comment:78
<p>
I don't mind if you close it---we now have type-nats of sorts, we can open future tickets for various improvements of them, if they are needed.
</p>
TicketbgamariWed, 16 Aug 2017 19:34:51 GMTstatus changed; resolution set
http://trac.haskell.org/trac/ghc/ticket/4385#comment:79
http://trac.haskell.org/trac/ghc/ticket/4385#comment:79
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Sounds good. Thanks yav!
</p>
Ticket