Type-level naturals #3058

kcsongor · 2017-08-29T23:19:29Z

A first attempt at implementing some of the features in #2899

This is incomplete - PR opened for discussion

Add kind Nat (with type-level literals)
Solve IsNat
Solve AddNat
multiplication / division
pow / root
conversion to a Peano encoding? Something like NatToPeano would allow to recurse on naturals easily - not sure how important this will be in the presence of instance chains though

this allows us to write

module Type.Data.Nat
  ( module Data.Nat
  , class AddNat
  , add
  , subtract
  ) where

import Data.Nat (NProxy(..), class IsNat, reflectNat, reifyNat)

class AddNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c, a c -> b, c b -> a

add :: forall a b c. AddNat a b c => NProxy a -> NProxy b -> NProxy c
add _ _ = NProxy

subtract :: forall a b c. AddNat a b c => NProxy c -> NProxy b -> NProxy a
subtract _ _ = NProxy

* Solve ConsSymbol This adds and solves a new 'magic' constraint, `Type.Data.Symbol.ConsSymbol`, with the following functional dependencies: class ConsSymbol (head :: Symbol) (tail :: Symbol) (sym :: Symbol) | sym -> head tail, head tail -> sym * The `head tail -> sym` direction works like `AppendSymbol`, but only resolves when `head` is a singleton symbol. * The `sym -> head tail` direction deconstructs the symbol into its first character and the remaining string. * Style fixes

* Add proxies * Add failing proxy test cases * Make proxy types of higher precedence * Proxy is no longer reserved * Move "proxy" to reservedTypeNames * s/proxy/@/g

* Add applicative do notation * Test the order of arguments to the result of an applicative do-block * Implement let statements in applicative do-blocks * Correctly handle PositionedDoNotationElement in applicative do-notation * Prefer map over pure when desugaring applicative do-notation * Delete AdoLetNotSupported variant

paf31 · 2017-09-10T00:14:58Z

How about putting the classes in Prim.Nat, since they don't have any members and therefore don't need any runtime dependencies?

…cript#3027)" (purescript#3030) This reverts commit 59d1c6a.

* Add instance chain groups * Make OverlappingInstances an error

* Add inlining for runEffFnN/mkEffFnN * Magic-do case to improve EffFn usage From natefaubion purescript#3026 (comment) * Apply magicDo until fixed point * Rearrange magic do optimizations * Stop run(Eff)FnX optimisation firing from local definitions * Add EffFn optimisation test

kcsongor · 2017-09-15T12:38:36Z

That makes sense, I'll do that. Does that mean that there are plans to move the Symbol classes into Prim too?

paf31 · 2017-09-15T17:42:04Z

I think AppendSymbol and CompareSymbol should probably go in Prim.Symbol, yes.

* Add kind Nat * Solve IsNat * Solve AddNat

paf31 · 2017-09-18T16:35:20Z

src/Language/PureScript/Constants.hs

+pattern TypeDataNat :: ModuleName
+pattern TypeDataNat = ModuleName [ProperName "Prim", ProperName "Nat"]
+
+pattern CompareNat :: Qualified (ProperName 'ClassName)


Can these move to Prim.Nat as well?

I should rename this patsyn to PrimNat, but as far as I can tell, all the purely typelevel classes are in Prim.Nat now - I didn't move IsNat, because it has a reifyNat function. Wouldn't that be a problem?

Great!

Wouldn't that be a problem?

Yes, it would, unless we find a better way to encode things. We could always say the integer is the dictionary, but then we wouldn't be able to write the class definition in such a way that people couldn't write bad instances.

You'll also need to add these to primClasses, and also add docstrings for them in the corresponding Docs module, so that they can be linked on Pursuit.

paf31 · 2017-10-02T18:28:03Z

@kcsongor Do you think this could be finished before we make a 0.12 release candidate? Skipping powers and roots wouldn't be the end of the world, I think, since we could implement those later. Also, NatToPeano could be implemented using instance chains for now, as you say. I think all that's left is to add the new data to the docs pages and to primClasses.

kcsongor · 2017-10-02T18:29:40Z

Oh, definitely. I’m going to update this tomorrow

kcsongor · 2017-10-02T18:48:17Z

Another question:

At the moment, we don't have polymorphic literals, which means that once we commit to Nat, we can't have Int with the same syntax, which would be a shame. How about changing these Nats to allow negative values (and call them Int accordingly), and Nat-ness could just be a constraint that the Int is greater than 0. This would mean that we would have an Int kind, and an additional IsNat class, which doesn't have to be solved by the compiler.

Implementation-wise, this is trivial, and I think it would allow us to cover more ground.

paf31 · 2017-10-02T18:53:24Z

How about changing these Nats to allow negative values (and call them Int accordingly), and Nat-ness could just be a constraint that the Int is greater than 0.

I feel like ints aren't as useful from a proving-things point of view. What induction principle would you use?

kcsongor · 2017-10-02T18:58:30Z

correction: Nats would be greater than or equal to 0.

Ints aren't as useful for that, but with instance chains, I think that shouldn't be a problem. What I mean is that these numbers can be treated like:

class IsNat n <= Induction (n :: Int) (p :: Int -> Type)

instance inductionZero :: Induction 0 p
else instance inductionS :: (IsNat n, Induction n p, Add n 1 m) => Induction m p

And negative numbers simply don't satisfy the superclass constraint.

paf31 · 2017-10-02T19:03:46Z

If you forget the IsNat constraint though, you'll end up spinning forever, right?

paf31 · 2017-10-02T19:05:31Z

You could always build the induction principle into IsNat, but I would say it's better to follow the maths and take Nat as the more primitive thing. I'm not terribly bothered about syntax, personally, since the type-level syntax isn't exactly pretty right now anyway.

kcsongor · 2017-10-02T19:10:14Z

If you forget the IsNat constraint though, you'll end up spinning forever, right?

Yes, that's a good point.

Int could also be implemented as a library, with the somewhat clumsier syntax:

foreign import kind Int
foreign import data Pos :: Nat -> Int
foreign import data Neg :: Nat -> Int

and I think Pos 10 and Neg 10 are not too bad.

LiamGoodacre · 2017-10-02T19:38:46Z

Annoyingly you get two zeros with that Pos 0/Neg 0. But that's possibly okay, depending on how it's handled/context.

paf31 · 2017-10-02T19:40:38Z

Negative and non-negative is another way to go, where Negative n means -(n + 1). Not exactly elegant though.

paf31 · 2017-10-02T19:41:36Z

The Grothendieck construction seems to be a nice way though, with an int being a pair of nats, with an equivalence relation such that only the signed difference matters.

kcsongor · 2017-10-10T12:31:12Z

@paf31 I've moved the classes to Prim. I tried to put them into Prim.Nat first, but I couldn't figure out how to convince the compiler that Prim.Nat is a valid class when importing it. If you could point me where this is done, I can change the imports.

As an additional point, the kind signature of CompareSymbol required the definition of the kind Ordering in Constants.hs.

Thanks

parsonsmatt · 2017-12-24T08:18:11Z

@kcsongor You might be interested in the work I did in #3176 with renaming the Prim classes. It's a bit hairier than you might expect.

kcsongor · 2017-12-24T08:33:21Z

Excellent, thanks! I could tell it was going to be a little hairy

natefaubion · 2018-10-23T02:55:15Z

This hasn't seen activity in some time. Should this be closed?

hdgarrood · 2019-02-15T01:54:47Z

I'm going to close this for now due to lack of movement, but I'll be happy to reopen if you manage to find time to pick this up again. For anyone else who might like to pick this up, please feel free to submit a new PR building on top of this too.

kcsongor and others added 3 commits September 9, 2017 15:36

Add proxies (purescript#2846)

74bc4a9

* Add proxies * Add failing proxy test cases * Make proxy types of higher precedence * Proxy is no longer reserved * Move "proxy" to reservedTypeNames * s/proxy/@/g

paf31 and others added 7 commits September 9, 2017 17:50

Remove scripts, fix purescript#2993 (purescript#3011)

eb0007d

Revert "Revert "Run AppendSymbol in reverse (purescript#3025)" (pures…

2a84878

…cript#3027)" (purescript#3030) This reverts commit 59d1c6a.

Update CONTRIBUTORS.md (purescript#3066)

305fbed

[purs ide] Groups hiding imports with implicit ones (purescript#3069)

46a3dcd

Instance chain groups (purescript#2929)

aacdb9a

* Add instance chain groups * Make OverlappingInstances an error

Remove old generics (purescript#3007)

fe6a098

Type-level naturals

7b3ea85

* Add kind Nat * Solve IsNat * Solve AddNat

kcsongor force-pushed the type-level-nats branch from 8a32cfc to 7b3ea85 Compare September 16, 2017 07:13

kcsongor added 2 commits September 16, 2017 08:15

Move type classes to Prim.Nat

5fd0c74

MultNat

9ffb15d

kcsongor force-pushed the type-level-nats branch from b535934 to 9ffb15d Compare September 16, 2017 07:23

paf31 reviewed Sep 18, 2017

View reviewed changes

paf31 added the needs more work label Sep 20, 2017

kcsongor added 2 commits October 4, 2017 12:42

Add PrimDoc for kind Nat

4cf93c0

Move Nat classes to Prim

9b5a0a3

paf31 force-pushed the master branch from 5c2463f to 2d974ba Compare November 5, 2017 20:58

matthewleon mentioned this pull request Jan 28, 2018

move Cardinality to type level purescript/purescript-enums#35

Closed

hdgarrood closed this Feb 15, 2019

purefunctor mentioned this pull request Nov 21, 2021

Type-level integers #4207

Merged

5 tasks

Type-level naturals #3058

Type-level naturals #3058

Uh oh!

Conversation

kcsongor commented Aug 29, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

paf31 commented Sep 10, 2017

Uh oh!

kcsongor commented Sep 15, 2017

Uh oh!

paf31 commented Sep 15, 2017

Uh oh!

paf31 Sep 18, 2017

Choose a reason for hiding this comment

Uh oh!

kcsongor Sep 18, 2017

Choose a reason for hiding this comment

Uh oh!

paf31 Sep 18, 2017

Choose a reason for hiding this comment

Uh oh!

paf31 Sep 20, 2017

Choose a reason for hiding this comment

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

kcsongor commented Oct 2, 2017

Uh oh!

kcsongor commented Oct 2, 2017

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

kcsongor commented Oct 2, 2017

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

kcsongor commented Oct 2, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

LiamGoodacre commented Oct 2, 2017

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

paf31 commented Oct 2, 2017

Uh oh!

kcsongor commented Oct 10, 2017

Uh oh!

parsonsmatt commented Dec 24, 2017

Uh oh!

kcsongor commented Dec 24, 2017

Uh oh!

natefaubion commented Oct 23, 2018

Uh oh!

hdgarrood commented Feb 15, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

kcsongor commented Aug 29, 2017 •

edited

Loading

kcsongor commented Oct 2, 2017 •

edited

Loading