Add toLinearN; narrow the coercion scope by treeowl · Pull Request #346 · tweag/linear-base

treeowl · 2021-10-04T17:28:13Z

Make toLinear, etc., explicitly coerce only multiplicities,
rather than whole arrow types. This is just a cleanup; it shouldn't
have any practical impact.
Add toLinearN and toLinearL to generalize toLinear, toLinear2, and toLinear3.

treeowl · 2021-10-04T17:35:35Z

Should we make at least some of these functions more polymorphic? I would think something like

toLinear
  :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
     (a :: TYPE r1) (b :: TYPE r2) p m x.
     (a %p-> b) %m-> (a %x-> b)

toLinear2
  :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (r3 :: RuntimeRep)
     (a :: TYPE r1) (b :: TYPE r2) (c :: TYPE r3) p q m x y.
     (a %p-> b %q-> c) %m-> (a %x-> b %y-> c)

toLinear3
  :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
     (r3 :: RuntimeRep) (r4 :: RuntimeRep)
     (a :: TYPE r1) (b :: TYPE r2) (c :: TYPE r3) (d :: TYPE r4) p q r m x y z.
     (a %p-> b %q-> c %r-> d) %m-> (a %x-> b %y-> c %z-> d)

This doesn't do much for toLinear, but for toLinear2 and toLinear3 I imagine something like this would be a considerable improvement.

treeowl · 2021-10-04T21:02:49Z

Since toLinearN is actually capable of changing multiplicities in any and all directions, should it have a different name?

treeowl · 2021-10-04T21:13:40Z

Might we want a version that takes a full list of multiplicity changes? Something like this?

toLinearList @'[ 'One :=> 'Many, _ :=> 'One, 'Many :=> n] ...

src/Unsafe/Linear.hs

aspiwack

I have a bunch of questions below. But I'm favourable to the change as a whole. As well as making the toLinearX functions returning functions of an arbitrary multiplicity (though maybe their name isn't ideal anymore, but it's not too serious).

I've got to admit, I'm feeling a bit of a mix of amazement and dismay that the Unsafe module is seeing such love 🙂 .

src/Unsafe/Linear.hs

aspiwack · 2021-10-05T07:08:53Z

src/Unsafe/Linear.hs

+-- | The actual implementation of 'ToLinearN', using the inductive natural
+-- number it's handed.
+type ToLinearN' :: forall {rep :: RuntimeRep}. INat -> TYPE rep -> TYPE rep -> Constraint
+class ToLinearN' arrs f g where
+  prf :: UnsafeEquality f g
+instance ToLinearN' k fb gb => ToLinearN' ('S k) ((a :: TYPE repa) %p-> (fb :: TYPE repb)) (a %q-> (gb :: TYPE repb)) where
+  prf = case prf @k @fb @gb of
+    UnsafeRefl -> case unsafeEqualityProof @p @q of
+      UnsafeRefl -> UnsafeRefl
+instance ToLinearN' 'Z (a :: TYPE rep) (a :: TYPE rep) where
+  prf = UnsafeRefl


Does this produce an O(n) irreducible proof? I'm not super up to date with the new unsafeEqualityProof mechanism.

And if so: is it bad?

The proof can get a bit long, but I don't think that we can do anything about it. It'll be erased in Core Prep or so.

src/Unsafe/Linear.hs

aspiwack · 2021-10-05T07:22:28Z

src/Unsafe/Linear.hs

+-- | @ToLinearL l f g@ means that @f@ and @g@ are the same with the
+-- possible exception of the multiplicities of some of the first arrows,
+-- as described by the list @l@.
+type ToLinearL :: forall {rep :: RuntimeRep}. [Change] -> TYPE rep -> TYPE rep -> Constraint
+class ToLinearL l f g where
+  -- | @unsafeLinearityProofL \@l \@f \@g @ is a fake proof that @f@ and @g@ are
+  -- the same with the possible exception of the multiplicities of the first
+  -- arrows given by the list @l@.
+  unsafeLinearityProofL :: UnsafeEquality f g
+instance ( ToLinearN' ni f g, UnifyL ni f g, UnifyL ni g f
+         , ni ~ Length l, UseChanges l f g) => ToLinearL l f g where
+  unsafeLinearityProofL = prf @ni


Is this really necessary? This can be achieved with a ToLinearN and a type annotation. I think that I'm essentially questioning the need for exporting an operator from this Unsafe module.

Yeah, you're right. Type application with plenty of underscores should be just as good.

aspiwack · 2021-10-05T07:42:05Z

@treeowl there appears to be an issue with CI. But I think I've fixed it in #348 , so you just need to rebase this PR and CI should start.

Make `toLinear`, etc., explicitly coerce only *multiplicities*, rather than whole arrow types. This is just a cleanup; it shouldn't have any practical impact.

treeowl · 2021-10-05T19:58:24Z

@aspiwack, I implemented your suggestions. Your suggested approach to ToLinearN' (with a heterogeneous equality tweak) is much better than what I was doing before. I also generalized the toLinear, toLinear2, and toLinear3 in a separate commit. I hope that doesn't wreak too much havoc on inference.

treeowl · 2021-10-05T20:01:11Z

Commits are now squashed to logical units.

aspiwack

Let's address the small comment below, then when you are happy, I'll merge.

src/Unsafe/Linear.hs

treeowl · 2021-10-06T07:04:05Z

I think this is ready to merge.

treeowl · 2021-10-06T07:05:33Z

Oh, I guess I should remove the word TODO...

Use the class system and some type-level hacking to generalize @toLinear@, @toLinear2@, and @toLinear3@.

This is mostly useful for `toLinear2` and `toLinear3`, where we may want to make *some* of the arrows linear but leave others as they are.

treeowl · 2021-10-06T07:11:43Z

OK, now it's really done.

aspiwack

Fantastic. Thanks a lot!

CI is green, which does mean that generalising the types of the unsafe operations hasn't been a problem in practice.

Let me merge now.

@utdemir it would be interesting to see if this PR has any effect on your benchmarks (I don't expect so, but you never know).

src/Unsafe/Linear.hs

treeowl force-pushed the toLinear branch from 9a4d970 to 0db5201 Compare October 4, 2021 17:29

treeowl force-pushed the toLinear branch from 277c93e to 3b06692 Compare October 4, 2021 21:09

treeowl changed the title ~~Narrow the unsafe coercion scope~~ Add toLinearN; narrow the coercion scope Oct 4, 2021

treeowl force-pushed the toLinear branch 2 times, most recently from ae770f5 to b0bf1a4 Compare October 4, 2021 21:28

treeowl commented Oct 4, 2021

View reviewed changes

src/Unsafe/Linear.hs Outdated Show resolved Hide resolved

treeowl force-pushed the toLinear branch from b0bf1a4 to ffb3cbb Compare October 4, 2021 21:31

treeowl changed the title ~~Add toLinearN; narrow the coercion scope~~ Add toLinearN/L; narrow the coercion scope Oct 5, 2021

aspiwack reviewed Oct 5, 2021

View reviewed changes

Narrow the unsafe coercion scope

195b77c

Make `toLinear`, etc., explicitly coerce only *multiplicities*, rather than whole arrow types. This is just a cleanup; it shouldn't have any practical impact.

treeowl force-pushed the toLinear branch 2 times, most recently from 0871ef8 to 466ace3 Compare October 5, 2021 19:54

treeowl force-pushed the toLinear branch from dcea31c to 1df5243 Compare October 5, 2021 20:00

treeowl force-pushed the toLinear branch 3 times, most recently from 9c88b2d to 3128aff Compare October 5, 2021 20:14

treeowl changed the title ~~Add toLinearN/L; narrow the coercion scope~~ Add toLinearN; narrow the coercion scope Oct 5, 2021

treeowl force-pushed the toLinear branch 3 times, most recently from 1703838 to 812286f Compare October 5, 2021 22:04

aspiwack approved these changes Oct 6, 2021

View reviewed changes

src/Unsafe/Linear.hs Show resolved Hide resolved

src/Unsafe/Linear.hs Outdated Show resolved Hide resolved

Add a generalization of toLinear

570752c

Use the class system and some type-level hacking to generalize @toLinear@, @toLinear2@, and @toLinear3@.

Generalize the types of toLinear, etc.

48d7c85

This is mostly useful for `toLinear2` and `toLinear3`, where we may want to make *some* of the arrows linear but leave others as they are.

treeowl force-pushed the toLinear branch from 812286f to 48d7c85 Compare October 6, 2021 07:09

aspiwack reviewed Oct 6, 2021

View reviewed changes

src/Unsafe/Linear.hs Show resolved Hide resolved

aspiwack merged commit 48816cb into tweag:master Oct 6, 2021

treeowl deleted the toLinear branch October 6, 2021 09:33

Conversation

treeowl commented Oct 4, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

treeowl commented Oct 4, 2021

Uh oh!

treeowl commented Oct 4, 2021

Uh oh!

treeowl commented Oct 4, 2021

Uh oh!

Uh oh!

aspiwack left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

aspiwack Oct 5, 2021

Choose a reason for hiding this comment

Uh oh!

treeowl Oct 5, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

aspiwack Oct 5, 2021

Choose a reason for hiding this comment

Uh oh!

treeowl Oct 5, 2021

Choose a reason for hiding this comment

Uh oh!

aspiwack commented Oct 5, 2021

Uh oh!

treeowl commented Oct 5, 2021

Uh oh!

treeowl commented Oct 5, 2021

Uh oh!

aspiwack left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

treeowl commented Oct 6, 2021

Uh oh!

treeowl commented Oct 6, 2021

Uh oh!

treeowl commented Oct 6, 2021

Uh oh!

aspiwack left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

treeowl commented Oct 4, 2021 •

edited

Loading