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
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
No, there's not another way to do this with built-in Nats, and there probably
won't ever be.
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
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,
Your argument here is compelling. I have wanted type-level integers from the
beginning and saw Nats as just a step toward integers. But, of course, this is
silly -- you're right that Nats deserve their own place.
Perhaps make a feature request for this. It may be related to type-level
pattern
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
If you define your own type level naturals by promoting
data Nat = Z | S Nat
you can define data families recursively, for example
data family Power :: Nat - * - *
data instance Power Z a = PowerZ
data instance Power (S n) a = PowerS a (Power n a)
But if you use the built-in type level Nat, I
you want the following (which doesnt require undediable instances)
data Nat = Z | S Nat
type family U (x :: Nat) where
U 0 = Z
U n = S (U (n-1))
this lets you convert type lits into your own peanos or whatever
hat tip to richard eisenburg for showing me this trick on the mailing list
a
because you haven't helped write a patch change it yet :)
-Carter
On Sat, Oct 25, 2014 at 9:53 AM, Barney Hilken b.hil...@ntlworld.com
wrote:
If you define your own type level naturals by promoting
data Nat = Z | S Nat
you can define data families recursively, for example
data family
you want the following (which doesnt require undediable instances)
data Nat = Z | S Nat
type family U (x :: Nat) where
U 0 = Z
U n = S (U (n-1))
this lets you convert type lits into your own peanos or whatever
Yes, you can do that, but why should you have to? Nat is already the
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)
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
12 matches
Mail list logo
