A more robust implementation of Replicator.elim#390
Conversation
|
I will take a look at it tomorrow morning! |
4d406d5 to
41ea515
Compare
tbagrel1
left a comment
There was a problem hiding this comment.
I just have questions at the moment (see review comments)
| -- has to solve. Look in particular at the instance @'IsFunN' a b (a' %p -> | ||
| -- f))@: it matches liberally, so triggers on quite underdetermined `f`, but has | ||
| -- equality constraints in its context which will help the type checker. | ||
| class IsFunN a b f |
There was a problem hiding this comment.
Couldn't we use something like
class IsFunN a b f where
type Arity
instance IsFunN a b b where
type Arity = 'Z
instance (IsFunN a b f, a' ~ a, p ~ 'One) => IsFunN a b (a' %p -> f) where
type Arity = 'S (Arity @a @b @f)to get rid of the explicit Arity type family ?
There was a problem hiding this comment.
I like the idea of having one class FunN to infer f from n a b, and one class IsFunN to infer n from a b f. Cheking IsFunN a b f should allow to compute the arity along the way (at least theorically).
There was a problem hiding this comment.
Did you manage to answer your own question? if so, I'm just waiting for the green tick so that I can merge.
There was a problem hiding this comment.
Yes, sorry
I thought that you wanted me to continue the work on this branch.
There was a problem hiding this comment.
I thought that you wanted me to continue the work on this branch.
I'll pretty never be asking you to continue work on a branch which passes tests 🙂 . If something is mergeable as it is, then we merge it. Merging small chunks early makes everybody's life easier.
41ea515 to
7b1d568
Compare
Use as `nix-shell --argstr "ghcVersion" "921"`.
This is really suspicious, there may be a bug in GHC 9.2 where sections do not preserve linearity. Grmpf.
I rely on more type families (I resurrected the `FunN` type family, for instance) and additional type classes in order to give robust hints to the type checker to infer some of the arguments based on the others in multiple possible ways. The previous version was abusing functional dependencies to that effect. The problem is that it almost certainly depended on bugs. Plus some behaviour changed in 9.2 making the recursive instance not typecheck anymore. The actual (staging) recursion now uses (type-level) Peano integers, this way we can get rid of the `OVERLAPPABLE` instances altogether, and avoid the sort of fragile behaviour that caused the failure in 9.2. The 'elim' function itself has more type arguments, so I took it out of the type class. A collection of type families and type classes fill the role that functional dependencies used to play: figuring out `f` from `n` or `n` from `f`. Fixes #388.
7b1d568 to
ad7b122
Compare
tbagrel1
left a comment
There was a problem hiding this comment.
After some time to process it, it looks good to me.
I rely on more type families (I resurrected the
FunNtype family,for instance) and additional type classes in order to give robust
hints to the type checker to infer some of the arguments based on the
others in multiple possible ways.
The previous version was abusing functional dependencies to that
effect. The problem is that it almost certainly depended on bugs. Plus
some behaviour changed in 9.2 making the recursive instance not
typecheck anymore.
The actual (staging) recursion now uses (type-level) Peano integers,
this way we can get rid of the
OVERLAPPABLEinstances altogether,and avoid the sort of fragile behaviour that caused the failure in
9.2.
The 'elim' function itself has more type arguments, so I took it out
of the type class. A collection of type families and type classes fill
the role that functional dependencies used to play: figuring out
ffrom
nornfromf.Fixes #388.
Interestingly I've only had to fix
Replicator.elimfor the sake offixing the compilation in GHC 9.2. The rest works fine. But it'd be
better to make similar changes to
V.makeandV.elim. I won't havetime to, though, @tbagrel1 can I untrust you with this?
I've made some additional small changes for the sake of GHC 9.2
compilation:
Minimal shell.nix changes to be able to run GHC 9.2
Some 𝜂-expansions to compile with GHC 9.2
This is really suspicious, there may be a bug in GHC 9.2 where
sections do not preserve linearity. Grmpf.