Remove linearity subtyping
It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes #73 (and maybe some others).
2020-12-27 22:58:35 +03:00
|
|
|
data MyNat : Type where
|
|
|
|
|
MyZ : MyNat
|
|
|
|
|
MyS : (1 _ : MyNat) -> MyNat
|
2020-05-19 20:25:18 +03:00
|
|
|
|
Remove linearity subtyping
It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes #73 (and maybe some others).
2020-12-27 22:58:35 +03:00
|
|
|
lplus : (1 x : MyNat) -> (1 y : MyNat) -> MyNat
|
|
|
|
|
lplus MyZ y = y
|
|
|
|
|
lplus (MyS k) y = MyS (lplus k y)
|
|
|
|
|
|
|
|
|
|
foo : (1 x : MyNat) -> (1 y : MyNat) -> MyNat -> MyNat
|
2020-05-19 20:25:18 +03:00
|
|
|
foo x y z
|
Remove linearity subtyping
It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes #73 (and maybe some others).
2020-12-27 22:58:35 +03:00
|
|
|
= let 1 test = the MyNat $ case z of
|
|
|
|
|
MyZ => MyZ
|
|
|
|
|
(MyS k) => MyS z
|
2020-05-19 20:25:18 +03:00
|
|
|
in
|
|
|
|
|
lplus test x
|