derp, my bad https://github.com/wellposed/numerical/blob/master/src/Numerical/Nat.hs has a fuller implementation of this though, that i've been using for a few months as for the plugin question, i think about adding constraint solves to the type system... so i dont know if thats quite what you want though, On Sat, Oct 25, 2014 at 2:33 PM, Barney Hilken wrote:

...

because you haven't helped write a patch change it yet :)

-Carter

Would this be possible with the new type checker plugins?

btw, your example gives me

Nested type family application in the type family application: U (n - 1) (Use UndecidableInstances to permit this) In the equations for closed type family ‘U’ In the type family declaration for ‘U’ Failed, modules loaded: none.

No, there's not another way to do this with built-in Nats, and there probably won't ever be.

I do hope you're wrong.

There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are unary and take up space linear in the value of the number. If you re-hash your proposal for a Successor constructor down to the term level, it looks juts like (n+k)-patterns, which were discarded as a bad idea.

(n+k) patterns are clearly a bad idea on integers, because the integers don't have the inductive structure, but they're a good idea on natural numbers, which is why they were in the language originally.

The reason that the type-level numbers are natural numbers and not integers is because natural numbers have a simpler theory to solve for. I'm personally hoping for proper type-level integers at some point, and the type-checker plugins approach may make that a reality sooner than later.

Type-level integers could well be useful, but they shouldn't replace type-level naturals, because they have completely different uses. At the value level, you can fudge the differences, because you can always return bottom, but at the type level you have to take correctness much more seriously if your type system is to be any use at all. The fact that Carter (and I) are forced to define hand-rolled nats on top of the built in ones demonstrates a clear need for this feature. It seems to me a valuable extension, whether the syntax uses Successor or (n+k). Why can't we combine the advantages of built-in Nats and hand-rolled ones? Barney.

Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 Unfortunately I don't know enough about ghc internals to try implementing it.

I don't think we'll need notation to differentiate: just use overloaded literals, like we do in terms. Something that would operate vaguely like this:

type family 3 :: k where 3 :: Nat = ... -- 3 as a Nat 3 :: Integer = ... -- 3 as an Integer

I'm not at all suggesting it be implemented this way, but we already have the ability to branch in type families based on result kind, so the mechanism is already around. Unfortunately, this would be unhelpful if the user asked for (3 :: Bool), which would kind-check but be stuck. Richard On Oct 28, 2014, at 8:24 PM, Iavor Diatchki wrote:

Hello,

actually type-level integers are easier to work with than type-level naturals (e.g., one can cancel things by subtracting at will). I agree that ideally we want to have both integers and naturals (probably as separate kinds). I just don't know what notation to use to distinguish the two.

-Iavor

On Mon, Oct 27, 2014 at 2:13 PM, Barney Hilken wrote: Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731

Unfortunately I don't know enough about ghc internals to try implementing it.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users