Opened 7 years ago

Last modified 15 months ago

#4385 new feature request

Type-level natural numbers

Reported by: diatchki Owned by: diatchki
Priority: normal Milestone:
Component: Compiler (Type checker) Version:
Keywords: Cc: alexey.skladnoy@…, sweirich@…, dimitris@…, byorgey@…, Conor.McBride@…, pumpkingod@…, as@…, leather@…, sjoerd@…, hesselink@…, erkokl@…, jeroen.weijers@…, conal@…, v.dijk.bas@…, helgikrs@…, nonowarn@…, djahandarie@…, christiaan.baaij@…, ghc@…, bjornbm, illissius@…, danlex@…, pho@…, dankna@…, favonia@…, jhenahan@…, reiner.pope@…, acfoltzer@…, nathanhowell@…, eir@…, douglas.mcclean@…, hvr@…, eric.pashman@…, Artyom.Kazak@…, j.stutterheim@…, mail@…, gregmainland@…, adamgundry, wren@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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).

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!

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).

Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:

  • a standard implementation,
  • a better notation,
  • better error messages,
  • a more efficient implementation,
  • more complete support for numeric operations.

I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:

http://code.galois.com/darcs/ghc-type-naturals/

Attachments (1)

Ticket.hs (786 bytes) - added by maltem 4 years ago.

Download all attachments as: .zip

Change History (77)

comment:1 Changed 6 years ago by igloo

Milestone: 7.2.1

comment:2 Changed 6 years ago by diatchki

The repos implementing this feature are now at this location:

http://code.galois.com/darcs/type-naturals/

A brief explanation of the implementation and how to use it as available here:

https://github.com/yav/memory-arrays/wiki

comment:3 Changed 6 years ago by simonpj

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:

  • I found integerToNat hard to grok. Could we use an existential instead?
    data DynNat where
      DN :: forall (n::Nat). Nat n -> DynNat
    integerToNat :: Integer -> DynNat
    
    Of course it's equivalent, but still.
  • We need to think systematically about syntax. You have
    • A kind Nat
    • A type Nat :: Nat -> *.
    • A type class TypeNat

And that's without thinking about a type-level equivalent of the kind Nat. At the type level we have 2 :: Nat. It's be much nicer if at the term level we also had 2 :: Nat (via the Num type class). But then the singleton type would have to be something different, Nat1, or SingleNat, or Single...?

The SHE notation (http://personal.cis.strath.ac.uk/~conor/pub/she/) uses the "braces of upward mobility" to promote values to types, and types to kinds. I wonder if we could use that somehow.

comment:4 in reply to:  3 Changed 6 years ago by diatchki

Replying to simonpj:

I wonder if you might use the GHC Trac Wiki instead?.

I moved the wiki pages to the GHC wiki: http://hackage.haskell.org/trac/ghc/wiki/TypeNats

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 http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors#Issues

comment:5 Changed 6 years ago by Khudyakov

Cc: alexey.skladnoy@… added

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{-1}. It's natural to encode dimensions using integer numbers.

This is not top priority item but I think it's good to keep such possibility in mind.

comment:6 Changed 6 years ago by adamgundry

Cc: adam.gundry@… added

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.

comment:7 in reply to:  description Changed 6 years ago by diatchki

Replying to diatchki: The most recently merged version of the implementation is at:

http://code.galois.com/darcs/type-naturals/09-Jan-2011/

The patches there are relative to GHC (and relevant libraries) as of 09-Jan-2011.

comment:8 Changed 6 years ago by simonpj

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.

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?

Simon

comment:9 Changed 6 years ago by diatchki

Hello,

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.

Briefly, my current status is:

  • 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 TODO list, so that we can write things like (a + b ~ c), rather then ((a + b) ~ c).
  • I've implemented the numeric type literals, which are of a new kind (currently called) Nat. I've added a new form of type LiteralTy TyLit, where TyLit 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.
  • I've added a set of operations on the type numbers, currently: comparison (<=), addition (+), multiplication (*), and exponentiation (^). 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.

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.

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?

  • In the support library, I made the DynNat 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 Natural, which mirrors Integer.

I think that that's all.

comment:10 Changed 6 years ago by simonpj

Cc: sweirich@… dimitris@… byorgey@… Conor.McBride@… added

Good! My suggestions for progress:

  • 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 DynNat.
  • Keep a wiki page, as you suggest, summarising design issues.

You already have these, I think, here http://hackage.haskell.org/trac/ghc/wiki/TypeNats, 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.

Email discussion belongs on cvs-ghc, I guess?

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 erasing 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.

Still the question remains of what evidence terms FC should have for numerics.

Iavor, if you continue to drive this, I'll be responsive. I'm adding Stephanie, Brent, Conor, Dimitrios to the cc list.

Simon

comment:11 Changed 6 years ago by pumpkin

Cc: pumpkingod@… added

comment:12 Changed 6 years ago by thoughtpolice

Cc: as@… added

comment:13 Changed 6 years ago by spl

Cc: leather@… added

comment:14 Changed 6 years ago by diatchki

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:

http://hackage.haskell.org/trac/ghc/wiki/TypeNats

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:

git clone git://code.galois.com/type-naturals/ghc.git

There are two branches in there, my work is on branch "type-nats" (branch "master" tracks the standrad GHC development branch).

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:

http://code.galois.com/darcs/type-naturals/09-Jan-2011/base
http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell

Usually, I use darcs-all to get the libraries from darcs.haskell.org, and then something like this:

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

Type-level nats are enabled with extensions TypeNaturals (e.g., -XTypeNaturals, or pragma LANGUAGE TypeNaturals.

comment:15 Changed 6 years ago by pumpkin

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?

I apologize if these questions are answered elsewhere, but I was unable to see anything much covering them.

I'm very excited by this development and look forward to tinkering with it as soon as I get some time, so thanks!

comment:16 Changed 6 years ago by diatchki

Hello,

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 :-).

unsafeCoerce 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.

comment:17 Changed 6 years ago by pumpkin

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).

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:

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 -}

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!

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

comment:18 Changed 6 years ago by adamgundry

Nice work! It's good to see some progress in this direction.

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?)

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:

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)

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.

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.

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

pure :: Nat n -> a -> Vec n a

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 TypeNats module abstraction barrier, but this is a bit clunky and inefficient.

comment:19 Changed 6 years ago by sjoerd_visscher

Cc: sjoerd@… added

comment:20 Changed 6 years ago by hesselink

Cc: hesselink@… added

comment:21 Changed 6 years ago by diatchki

Hello,

I added some support for associativity over the weekend, and now the (+++) example works (I've pushed the changes to the git repo).

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: http://hackage.haskell.org/trac/ghc/wiki/TypeNats/InductiveDefinitions We might even be able to add a "fold" to deforest the intermediate "Zero" and "Succ" constructors.

(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.)

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).

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:

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.. 

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.

comment:22 Changed 6 years ago by lerkok

Cc: erkokl@… added

Let me briefly chime in an express great interest in this project. Iavor has been able to pull in the sbv package (http://hackage.haskell.org/package/sbv) 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.)

comment:23 Changed 6 years ago by jweijers

Cc: jeroen.weijers@… added

comment:24 Changed 6 years ago by conal

Cc: conal@… added

comment:25 Changed 6 years ago by basvandijk

Cc: v.dijk.bas@… added

comment:26 Changed 6 years ago by helgikrs

Cc: helgikrs@… added

comment:27 Changed 6 years ago by nwn

Cc: nonowarn@… added

comment:28 Changed 6 years ago by djahandarie

Cc: djahandarie@… added

comment:29 Changed 6 years ago by ChristiaanBaaij

Cc: christiaan.baaij@… added

comment:30 Changed 6 years ago by Lemming

Cc: ghc@… added

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. :-)

comment:31 in reply to:  3 Changed 6 years ago by jeltsch

Replying to simonpj:

I really, really want to make operators into type constructors rather than (as at present) type variables. So that we can write a type (a + b) rather than (a :+ b). See http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors. Doing this is, I think, straightforward, but it still needs doing.

Really nice. What GHC version can be expected to have this feature? I’d like to use it.

comment:32 Changed 6 years ago by bjornbm

Cc: bjornbm added

comment:33 Changed 6 years ago by illissius

Cc: illissius@… added

comment:34 Changed 6 years ago by FSalad

Cc: danlex@… added

comment:35 Changed 6 years ago by PHO

Cc: pho@… added

comment:36 Changed 6 years ago by dankna

Cc: dankna@… added

comment:37 Changed 6 years ago by Favonia

Cc: favonia@… added

comment:38 Changed 6 years ago by dankna

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.

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.

Here's what I'm doing:

data IntType :: * -> Nat -> *
data Negative
data NonNegative
class IntClass int
instance IntClass (IntType NonNegative num)
instance (1 <= num) => IntClass (IntType Negative num)

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:

type family MinusNat a b
type instance MinusNat (ab ~ a + b) b = a

or alternatively

type family MinusNat a b
type instance (ab ~ a + b) => MinusNat ab b = a

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.

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.

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.

comment:39 Changed 6 years ago by jeltsch

Would it be possible to name the new kind Natural instead of Nat? That way, the naming would be consistent with the naming of integer types, where Int only refers to a subset of the integers, while Integer refers to the complete set.

comment:40 in reply to:  39 ; Changed 6 years ago by jhenahan

Cc: jhenahan@… added

Replying to jeltsch:

Would it be possible to name the new kind Natural instead of Nat? That way, the naming would be consistent with the naming of integer types, where Int only refers to a subset of the integers, while Integer refers to the complete set.

Cf. Agda.

comment:41 in reply to:  40 Changed 6 years ago by jeltsch

Replying to jhenahan:

Replying to jeltsch:

Would it be possible to name the new kind Natural instead of Nat? That way, the naming would be consistent with the naming of integer types, where Int only refers to a subset of the integers, while Integer refers to the complete set.

Cf. Agda.

Hmm, the type of natural numbers is called ℕ in Agda. Well, the module it’s defined in is called Data.Nat. But why should Haskell be consistent with Agda, but not consistent with itself?

comment:42 in reply to:  38 Changed 6 years ago by sjoerd_visscher

Replying to dankna:

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.

Have you tried defining type-level integer in terms of 2 type-level naturals, the value being the difference between the 2 naturals:

data IntType :: Nat -> Nat -> *

type family Minus a b
type instance Minus (IntType a b) (IntType c d) = IntType (a + d) (b + c)

The type for f.e. -2 would then be forall n. IntType n (n + 2).

comment:43 Changed 6 years ago by dankna

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?

comment:44 Changed 6 years ago by sjoerd_visscher

Instead of (i ~ IntType Negative 2) you get (i ~ IntType n (n + 2)).

comment:45 Changed 6 years ago by reinerp

Cc: reiner.pope@… added

comment:46 Changed 6 years ago by acfoltzer

Cc: acfoltzer@… added

comment:47 Changed 5 years ago by nathanhowell

Cc: nathanhowell@… added

comment:48 Changed 5 years ago by bjornbm

It seems this ticket needs an update by someone in the know. I understand TypeNats didn't make it into 7.4.1 in the end so at least the milestone is inaccurate(?). Can we still expect to see TypeNats in GHC?

comment:49 Changed 5 years ago by diatchki

Hello,

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.

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.

comment:50 Changed 5 years ago by igloo

Milestone: 7.4.17.6.1

comment:51 Changed 5 years ago by goldfire

Cc: eir@… added

comment:52 Changed 5 years ago by dmcclean

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.

comment:53 Changed 5 years ago by dmcclean

Cc: douglas.mcclean@… added

comment:54 Changed 5 years ago by carter

wait.... theres no constraint solver in yet? that would explain why I had the bugs I reported wrt type nats last week!

comment:55 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:56 Changed 4 years ago by hvr

Cc: hvr@… added

comment:57 Changed 4 years ago by pash

Cc: eric.pashman@… added

comment:58 Changed 4 years ago by maltem

I'm trying out the type-nats branch and the wiki says to complain when the solver cannot solve something, so here we go:

Bug.hs:22:29:
    Could not deduce ((2 * n) ~ ((2 * n1) + 2))
    from the context (n ~ (n1 + 1))

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).

Changed 4 years ago by maltem

Attachment: Ticket.hs added

comment:59 Changed 4 years ago by diatchki

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 ns somehow, it'd get solved, but I know that's not always an option.

comment:60 Changed 4 years ago by darchon

I get a similar error implementing concat for vectors:

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)

comment:61 Changed 4 years ago by Artyom.Kazak

Cc: Artyom.Kazak@… added

comment:62 Changed 4 years ago by guest

Is there a way to make the following work?

Couldn't match type `1 + 0' with `1'

Here is a test to reproduce this.

(test2 and test3 produce the errors when the line that don't work are uncommented) This is a file:

--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 

comment:63 Changed 4 years ago by norm2782

Cc: j.stutterheim@… added
difficulty: Unknown

comment:64 Changed 4 years ago by nsch

Cc: mail@… added

comment:65 Changed 4 years ago by ghorn

Cc: gregmainland@… added

comment:66 Changed 3 years ago by Lemming

Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in

http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/

comment:67 in reply to:  66 ; Changed 3 years ago by hvr

Replying to Lemming:

Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in

http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/

does http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals count?

comment:68 in reply to:  67 Changed 3 years ago by Lemming

Replying to hvr:

Replying to Lemming:

Type-level natural numbers are advertised everywhere for GHC-7.8, but I cannot find documentation in

http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/

does http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/promotion.html#promoted-literals count?

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:

https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Basics https://ghc.haskell.org/trac/ghc/wiki/TypeNats/Operations

Do these articles reflect the current state of implementation?

I also found the announcement:

http://www.well-typed.com/blog/85

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.

comment:69 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:70 Changed 2 years ago by thoughtpolice

Milestone: 7.10.17.12.1

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.

comment:71 Changed 2 years ago by dmcclean

Could anyone provide an update on the current state of efforts to improve the constraint solver?

comment:72 Changed 2 years ago by adamgundry

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: https://github.com/yav/type-nat-solver

More generally, the aim of the typechecker plugins work is to make this sort of thing easier to experiment with.

comment:73 Changed 2 years ago by adamgundry

Cc: adamgundry added; adam.gundry@… removed

comment:74 Changed 20 months ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:75 Changed 20 months ago by WrenThornton

Cc: wren@… added

comment:76 Changed 15 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.