... | ... | @@ -56,52 +56,49 @@ type instance F Bool Int Char = Char |
|
|
```
|
|
|
|
|
|
1. Injectivity in some of the arguments, where knowing the RHS of a type
|
|
|
family determines only some of the arguments on the LHS. Example:
|
|
|
|
|
|
```haskell
|
|
|
type family G a b c
|
|
|
type instance G Int Char Bool = Bool
|
|
|
type instance G Int Char Int = Bool
|
|
|
type instance G Bool Int Int = Int
|
|
|
```
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Here knowing the RHS allows us to determine first two arguments, but not the
|
|
|
> third one.
|
|
|
>
|
|
|
>
|
|
|
family determines only some of the arguments on the LHS. Example:
|
|
|
|
|
|
```haskell
|
|
|
type family G a b c
|
|
|
type instance G Int Char Bool = Bool
|
|
|
type instance G Int Char Int = Bool
|
|
|
type instance G Bool Int Int = Int
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
Here knowing the RHS allows us to determine first two arguments, but not the
|
|
|
third one.
|
|
|
|
|
|
|
|
|
|
|
|
1. Injectivity in some of the arguments, where knowing the RHS of a type
|
|
|
family and some of the LHS arguments determines other (possibly not all)
|
|
|
LHS arguments. Examples:
|
|
|
|
|
|
```haskell
|
|
|
type family Plus a b where
|
|
|
Plus Z n = n
|
|
|
Plus (S m) n = S (Plus m n)
|
|
|
```
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Here knowing the RHS and the first argument uniquely determines the remaining
|
|
|
> argument.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
```haskell
|
|
|
type family H a b c
|
|
|
type instance H Int Char Double = Int
|
|
|
type instance H Bool Double Double = Int
|
|
|
```
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Knowing the RHS and either `a` or `b` allows to uniquely determine the
|
|
|
> remaining two arguments, but knowing the RHS and `c` gives us no information
|
|
|
> about `a` or `b`.
|
|
|
>
|
|
|
>
|
|
|
family and some of the LHS arguments determines other (possibly not all)
|
|
|
LHS arguments. Examples:
|
|
|
|
|
|
```haskell
|
|
|
type family Plus a b where
|
|
|
Plus Z n = n
|
|
|
Plus (S m) n = S (Plus m n)
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
Here knowing the RHS and the first argument uniquely determines the remaining
|
|
|
argument.
|
|
|
|
|
|
|
|
|
|
|
|
```haskell
|
|
|
type family H a b c
|
|
|
type instance H Int Char Double = Int
|
|
|
type instance H Bool Double Double = Int
|
|
|
```
|
|
|
Knowing the RHS and either `a` or `b` allows to uniquely determine the
|
|
|
remaining two arguments, but knowing the RHS and `c` gives us no information
|
|
|
about `a` or `b`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In the following text I will refer to these three forms of injectivity as A, B
|
... | ... | @@ -228,18 +225,18 @@ annotation then we conclude that a type family is not injective in a way user |
|
|
claims and we report an error.
|
|
|
|
|
|
1. If a RHS of a type family equation is a type family application we conclude
|
|
|
that the type family is not injective.
|
|
|
that the type family is not injective.
|
|
|
|
|
|
1. If a RHS of a type family equation is a bare type variable we require that
|
|
|
all LHS variables (including implicit kind variables) are also bare. In
|
|
|
other words, this has to be a sole equation of that type family and it has to
|
|
|
cover all possible patterns. If the patterns are not covering we conclude
|
|
|
that the type family is not injective.
|
|
|
all LHS variables (including implicit kind variables) are also bare. In
|
|
|
other words, this has to be a sole equation of that type family and it has to
|
|
|
cover all possible patterns. If the patterns are not covering we conclude
|
|
|
that the type family is not injective.
|
|
|
|
|
|
1. If a LHS type variable that is declared as injective is not mentioned on
|
|
|
injective position in the RHS we conclude that the type family is not
|
|
|
injective. By "injective position" we mean argument to a type constructor or
|
|
|
argument to a type family on injective position.
|
|
|
injective position in the RHS we conclude that the type family is not
|
|
|
injective. By "injective position" we mean argument to a type constructor or
|
|
|
argument to a type family on injective position.
|
|
|
|
|
|
Open type families (including associated types)
|
|
|
|
... | ... | @@ -251,10 +248,10 @@ checking equations pair-wise (a new equation against all already checked |
|
|
equations -- modulo optimisations).
|
|
|
|
|
|
1. When checking a pair of an open type family equations we attempt to unify
|
|
|
their RHSs. If they don't unify this pair does not violate injectivity
|
|
|
annotation. If unification succeeds with a substitution (possibly empty)
|
|
|
then LHSs of unified equations must be identical under that substitution. If
|
|
|
they are not identical then we conclude that a type family is not injective.
|
|
|
their RHSs. If they don't unify this pair does not violate injectivity
|
|
|
annotation. If unification succeeds with a substitution (possibly empty)
|
|
|
then LHSs of unified equations must be identical under that substitution. If
|
|
|
they are not identical then we conclude that a type family is not injective.
|
|
|
|
|
|
|
|
|
Note that we use a special variant of the unification algorithm that treats type
|
... | ... | @@ -269,11 +266,11 @@ the preceeding equations. Of course a single-equation closed type family is |
|
|
trivially injective (unless (1), (2) or (3) above holds).
|
|
|
|
|
|
1. When checking a pair of closed type family equations we try to unify their
|
|
|
RHSs. If they don't unify this pair does not violate injectivity annotation.
|
|
|
If the RHSs can be unified under some substitution (possibly empty) then
|
|
|
either the LHSs unify under the same substitution or the LHS of the latter
|
|
|
equation is subsumed by earlier equations. If neither condition is met we
|
|
|
conclude that a type family is not injective.
|
|
|
RHSs. If they don't unify this pair does not violate injectivity annotation.
|
|
|
If the RHSs can be unified under some substitution (possibly empty) then
|
|
|
either the LHSs unify under the same substitution or the LHS of the latter
|
|
|
equation is subsumed by earlier equations. If neither condition is met we
|
|
|
conclude that a type family is not injective.
|
|
|
|
|
|
|
|
|
Again, we use a special variant of the unification algorithm.
|
... | ... | @@ -383,531 +380,189 @@ relevant emails here so they don't get lost and are available to anyone who |
|
|
decides to take up the work.
|
|
|
|
|
|
|
|
|
|
|
|
Richard Eisenber, 16 July 2015:
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Here is an interesting case:
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> type family F a b = r \| r a -\> b where
|
|
|
>
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > F Int a = Maybe (F a Int)
|
|
|
> > F Bool a = \[a\]
|
|
|
> > F Char a = \[a\]
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> ```haskell
|
|
|
> type family F a b = r | r a -> b where
|
|
|
> F Int a = Maybe (F a Int)
|
|
|
> F Bool a = [a]
|
|
|
> F Char a = [a]
|
|
|
> ```
|
|
|
>
|
|
|
> This should be rejected, because of the following facts:
|
|
|
>
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > F Int Bool \~ Maybe \[Int\]
|
|
|
> > F Int Char \~ Maybe \[Int\]
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
>
|
|
|
> ```haskell
|
|
|
> F Int Bool ~ Maybe [Int]
|
|
|
> F Int Char ~ Maybe [Int]
|
|
|
> ```
|
|
|
> Thus, the first parameter and the result do not, in concert, uniquely determine the second parameter.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> Yet Simon's "just tuple them up" approach would label F as injective. The only interesting pairwise check is the first equation against itself. We run this:
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > U( ( (Int, Maybe (F a Int)), (Int, Maybe (F b Int)) )
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> <table><tr><td>If we are to recur into F via equation (7), then we get a substitution [a> b], and the pairwise check (erroneously) succeeds. Simon said that the arguments to the left of -> need to be syntactically identical, which this case fails. But now consider this:
|
|
|
> </td></tr></table>
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> type family G a b = r \| r a -\> b where
|
|
|
>
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > G Int (a,b) = (Maybe (G a b), a)
|
|
|
> > G Bool a = \[a\]
|
|
|
> > G Char a = \[a\]
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > U( (Int, (Maybe (G a b), a)) , (Int, (Maybe (G c d), c)) )
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> <table><tr><td>Here, it is OK to recur via equation (7), because the presence of a and c outside of the recursive call gets them to unify. Indeed we must recur to accept G, because we need to look under G to get the mapping [b> d]. (The fundep version of F is rejected and the fundep version of G is accepted.)
|
|
|
> </td></tr></table>
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> ```
|
|
|
> U( ( (Int, Maybe (F a Int)), (Int, Maybe (F b Int)) )
|
|
|
> ```
|
|
|
>
|
|
|
> If we are to recur into F via equation (7), then we get a substitution `[a |-> b]`, and the pairwise check (erroneously) succeeds. Simon said that the arguments to the left of -> need to be syntactically identical, which this case fails. But now consider this:
|
|
|
>
|
|
|
> ```haskell
|
|
|
> type family G a b = r | r a -> b where
|
|
|
> G Int (a,b) = (Maybe (G a b), a)
|
|
|
> G Bool a = [a]
|
|
|
> G Char a = [a]
|
|
|
>
|
|
|
> U( (Int, (Maybe (G a b), a)) , (Int, (Maybe (G c d), c)) )
|
|
|
> ```
|
|
|
>
|
|
|
> Here, it is OK to recur via equation (7), because the presence of a and c outside of the recursive call gets them to unify. Indeed we must recur to accept G, because we need to look under G to get the mapping [b |-> d]. (The fundep version of F is rejected and the fundep version of G is accepted.)
|
|
|
>
|
|
|
> I believe this G exemplifies the order-dependency Jan was worried about. We somehow need to unify the second component of that tuple before looking under G.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> So the question is: when can equation (7) apply?
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> I naturally tried to answer this myself, via comparison with functional dependencies. My guess was that our check is a little more liberal than the fundep check, in that we accept benign overlap between equations. When I pushed this on the fundep side, I discovered that fundeps as implemented in 7.10.1 are broken! Here is the test case:
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
|
|
|
FlexibleInstances, UndecidableInstances #-}
|
|
|
|
|
|
module FD where
|
|
|
|
|
|
class H a b r | a b -> r, r a -> b
|
|
|
instance H Bool Double Bool
|
|
|
|
|
|
class G a b c r | a b c -> r, r a -> b
|
|
|
instance H a b r => G Int (a,b) () (Maybe r, a)
|
|
|
instance G Int (a,a) Char (Maybe a, a)
|
|
|
|
|
|
foo :: G a b c r => (a,b,c,r)
|
|
|
foo = undefined
|
|
|
|
|
|
-- (1): instance G Int (Bool, Bool) Char (Maybe Bool, Bool)
|
|
|
x = foo :: (Int, (Bool, Bool), Char, (Maybe Bool, Bool))
|
|
|
|
|
|
-- (2): instance G Int (Bool, Double) () (Maybe Bool, Bool)
|
|
|
y = foo :: (Int, (Bool, Double), (), (Maybe Bool, Bool))
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> This compiles in 7.10.1. Yet we can see that GHC finds instances (1) and (2) marked above, even though these violate the second functional dependency on G: r and a do \*not\* uniquely determine b. (The c parameter is there simply to avoid overlapping instances.)
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> So perhaps the story \*is\* rather more complicated than we thought, and fundeps' simplicity in this matter is bogus.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> ```haskell
|
|
|
> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
|
|
|
> FlexibleInstances, UndecidableInstances #-}
|
|
|
>
|
|
|
> module FD where
|
|
|
>
|
|
|
> class H a b r | a b -> r, r a -> b
|
|
|
> instance H Bool Double Bool
|
|
|
>
|
|
|
> class G a b c r | a b c -> r, r a -> b
|
|
|
> instance H a b r => G Int (a,b) () (Maybe r, a)
|
|
|
> instance G Int (a,a) Char (Maybe a, a)
|
|
|
>
|
|
|
> foo :: G a b c r => (a,b,c,r)
|
|
|
> foo = undefined
|
|
|
>
|
|
|
> -- (1): instance G Int (Bool, Bool) Char (Maybe Bool, Bool)
|
|
|
> x = foo :: (Int, (Bool, Bool), Char, (Maybe Bool, Bool))
|
|
|
>
|
|
|
> -- (2): instance G Int (Bool, Double) () (Maybe Bool, Bool)
|
|
|
> y = foo :: (Int, (Bool, Double), (), (Maybe Bool, Bool))
|
|
|
> ```
|
|
|
>
|
|
|
> This compiles in 7.10.1. Yet we can see that GHC finds instances (1) and (2) marked above, even though these violate the second functional dependency on G: r and a do *not* uniquely determine b. (The c parameter is there simply to avoid overlapping instances.)
|
|
|
>
|
|
|
> So perhaps the story *is* rather more complicated than we thought, and fundeps' simplicity in this matter is bogus.
|
|
|
>
|
|
|
> And, quite separately, I'm also worried about the bare-type-variable-on-the-right problem. But let's solve this before tackling that.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
Simon Peyton Jones, 23rd July 2015:
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> I'm being slow here, but I have learned some things.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. As you'll see from "Understanding FDs using CHRs", we have to check
|
|
|
TWO things for FDs:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > class C a b \| a -\> b
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Coverage: for each instance, individually, check coverage
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > instance Q =\> C s t
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
>
|
|
|
> The naïve version just checks that fvs(s) is a superset of fvs(t).
|
|
|
> The "liberal" coverage condition takes account of Q.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Consistency: compare all instances pairwise to check that they are consistent
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > instance Q1 =\> C s1 t1
|
|
|
> > instance Q2 =\> C s2 t2
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
>
|
|
|
> if S = unify(s1,s2), then check that S(t1) = S(t2)
|
|
|
> Notice that this does not take account of Q1, S2 at all.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. In our paper we have ONE check. But I believe that
|
|
|
|
|
|
- consistency = comparing equations i,j, where i is \*distinct\* from j
|
|
|
- coverage = comparing equation I with itself
|
|
|
|
|
|
So that makes our approach rather nicely uniform.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. GHC has an outright bug in its handling of consistency,
|
|
|
as you both point out. But it's a bug that seems to be exploited!
|
|
|
See Trac #10675.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. For \*consistency\*, our approach is a little more liberal than FDs,
|
|
|
because the FD stuff takes no account of Q1, Q2. Example
|
|
|
(in type-family form)
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > F (a,Int) = (\[G a\], Maybe Int)
|
|
|
> > F (Bool,b) = (\[G Bool\], Maybe b)
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
>
|
|
|
> where G is injective, and F is claimed to be.
|
|
|
> We find that F is injective because, using the injectivity
|
|
|
> of G, we unify a:=Bool.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > But in FD form
|
|
|
> >
|
|
|
> >
|
|
|
> > >
|
|
|
> > >
|
|
|
> > > class F a r \| r -\> a
|
|
|
> > > instance G a r =\> F (a,Int) (\[r\], Maybe Int)
|
|
|
> > > instance G Bool r =\> F (Bool,b) (\[r\], Maybe b)
|
|
|
> > >
|
|
|
> > >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > These two will be rejected by the FD world because of
|
|
|
> > ignoring Q1, Q2.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > That said, I don't think this additional expressiveness
|
|
|
> > is very useful. The BIG thing about our ability to exploit
|
|
|
> > injectivity comes when comparing an equation with itself i=j.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. For \*coverage\*, the "liberal" coverage condition behaves
|
|
|
very like our "exploiting injectivity in algorithm U" idea.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > However if we extend to injectivity constraints like
|
|
|
> >
|
|
|
> >
|
|
|
> > >
|
|
|
> > >
|
|
|
> > > a r -\> b
|
|
|
> > >
|
|
|
> > >
|
|
|
> >
|
|
|
> >
|
|
|
> > then, as you both point out, we'll need some kind of
|
|
|
> > iterative scheme. Suppose we have
|
|
|
> >
|
|
|
> >
|
|
|
> > >
|
|
|
> > >
|
|
|
> > > type family F a b = r \| r a -\> b
|
|
|
> > >
|
|
|
> > >
|
|
|
> >
|
|
|
> >
|
|
|
> > Then Rule (7) would become something like
|
|
|
> >
|
|
|
> >
|
|
|
> > >
|
|
|
> > >
|
|
|
> > > U(F s1 s2, F t1 t2) T = U(s2,t2) T, if T(s1)=T(t1)
|
|
|
> > >
|
|
|
> > >
|
|
|
> >
|
|
|
> >
|
|
|
> > and the side condition (syntactic equality) might change
|
|
|
> > as unification progresses.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > What happens for coverage for fudeps? We don't use unification;
|
|
|
> > we use free variables, as in Defn 7 of the paper. But crucially
|
|
|
> > we use an iterative algorithm that iterates to a fixpoint;
|
|
|
> > see [FunDeps](fun-deps).oclose.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > We would have to do the same, in some form.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> 1. As you'll see from "Understanding FDs using CHRs", we have to check
|
|
|
> TWO things for FDs:
|
|
|
>
|
|
|
> ```
|
|
|
> class C a b | a -> b
|
|
|
> ```
|
|
|
>
|
|
|
> * Coverage: for each instance, individually, check coverage
|
|
|
> instance Q => C s t
|
|
|
> The naïve version just checks that fvs(s) is a superset of fvs(t).
|
|
|
> The "liberal" coverage condition takes account of Q.
|
|
|
>
|
|
|
> * Consistency: compare all instances pairwise to check that they are consistent
|
|
|
> ```haskell
|
|
|
> instance Q1 => C s1 t1
|
|
|
> instance Q2 => C s2 t2
|
|
|
> ```
|
|
|
> if S = unify(s1,s2), then check that S(t1) = S(t2)
|
|
|
> Notice that this does not take account of Q1, S2 at all.
|
|
|
>
|
|
|
>
|
|
|
> 2. In our paper we have ONE check. But I believe that
|
|
|
> - consistency = comparing equations i,j, where i is *distinct* from j
|
|
|
> - coverage = comparing equation I with itself
|
|
|
> So that makes our approach rather nicely uniform.
|
|
|
>
|
|
|
>
|
|
|
> 3. GHC has an outright bug in its handling of consistency,
|
|
|
> as you both point out. But it's a bug that seems to be exploited!
|
|
|
> See Trac #10675.
|
|
|
>
|
|
|
> 4. For *consistency*, our approach is a little more liberal than FDs,
|
|
|
> because the FD stuff takes no account of Q1, Q2. Example
|
|
|
> (in type-family form)
|
|
|
> ```haskell
|
|
|
> F (a,Int) = ([G a], Maybe Int)
|
|
|
> F (Bool,b) = ([G Bool], Maybe b)
|
|
|
> ```
|
|
|
> where G is injective, and F is claimed to be.
|
|
|
> We find that F is injective because, using the injectivity
|
|
|
> of G, we unify a:=Bool.
|
|
|
>
|
|
|
> But in FD form
|
|
|
> ```haskell
|
|
|
> class F a r | r -> a
|
|
|
> instance G a r => F (a,Int) ([r], Maybe Int)
|
|
|
> instance G Bool r => F (Bool,b) ([r], Maybe b)
|
|
|
> ```
|
|
|
>
|
|
|
> These two will be rejected by the FD world because of
|
|
|
> ignoring Q1, Q2.
|
|
|
>
|
|
|
> That said, I don't think this additional expressiveness
|
|
|
> is very useful. The BIG thing about our ability to exploit
|
|
|
> injectivity comes when comparing an equation with itself i=j.
|
|
|
>
|
|
|
> 5. For *coverage*, the "liberal" coverage condition behaves
|
|
|
> very like our "exploiting injectivity in algorithm U" idea.
|
|
|
>
|
|
|
> However if we extend to injectivity constraints like
|
|
|
> a r -> b
|
|
|
> then, as you both point out, we'll need some kind of
|
|
|
> iterative scheme. Suppose we have
|
|
|
> type family F a b = r | r a -> b
|
|
|
> Then Rule (7) would become something like
|
|
|
> U(F s1 s2, F t1 t2) T = U(s2,t2) T, if T(s1)=T(t1)
|
|
|
> and the side condition (syntactic equality) might change
|
|
|
> as unification progresses.
|
|
|
>
|
|
|
> What happens for coverage for fudeps? We don't use unification;
|
|
|
> we use free variables, as in Defn 7 of the paper. But crucially
|
|
|
> we use an iterative algorithm that iterates to a fixpoint;
|
|
|
> see FunDeps.oclose.
|
|
|
>
|
|
|
> We would have to do the same, in some form.
|
|
|
>
|
|
|
> Questions:
|
|
|
>
|
|
|
>
|
|
|
|
|
|
- FDs uses different technology for the coverage (i/i) and
|
|
|
consistency (i/j) tests. We could do so too; after all,
|
|
|
in the i/I case we know that the type structure matches!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Do we really care about the extra expressiveness of rule (7)
|
|
|
for the (i/j) case?
|
|
|
|
|
|
> - FDs uses different technology for the coverage (i/i) and
|
|
|
> consistency (i/j) tests. We could do so too; after all,
|
|
|
> in the i/I case we know that the type structure matches!
|
|
|
>
|
|
|
> - Do we really care about the extra expressiveness of rule (7)
|
|
|
> for the (i/j) case?
|
|
|
|
|
|
Simon Peyton Jones, 24rd July 2015:
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Jan says (and I can see) that we ALREADY use different
|
|
|
> mechanisms for i/j and i/i.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
>
|
|
|
> So I propose that:
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- We elaborate the i/i (coverage) test to do the iterative
|
|
|
'oclose' thing. This already does not use algorithm U at all.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- We simplify algorithm U by dropping Rule (7) altogether.
|
|
|
|
|
|
- U is only used for i/j tests
|
|
|
- it's hard to craft an example where Rule (7) matters
|
|
|
- even such examples that exist are terribly fragile
|
|
|
(e.g. in my point (4) if I replace (G Bool) by its
|
|
|
values, say Char, then the test will fail)
|
|
|
|
|
|
>
|
|
|
> * We elaborate the i/i (coverage) test to do the iterative
|
|
|
> 'oclose' thing. This already does not use algorithm U at all.
|
|
|
>
|
|
|
> * We simplify algorithm U by dropping Rule (7) altogether.
|
|
|
> - U is only used for i/j tests
|
|
|
> - it's hard to craft an example where Rule (7) matters
|
|
|
> - even such examples that exist are terribly fragile
|
|
|
> (e.g. in my point (4) if I replace (G Bool) by its
|
|
|
> values, say Char, then the test will fail)
|
|
|
|
|
|
Richard Eisenber, 26 July 2015:
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Simon has come to the same conclusions I have while pondering this all: we differ from FDs in that we cleverly use the same pairwise check between two different equations as we do when comparing an equation against itself. But this is perhaps too clever, and perhaps explains why the proof has foundered around this very issue (that is, equation 7).
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
|
|
|
> So, I agree with Simon's proposal: explain all of this in terms of two separate checks. One check does a coverage check (very like the FD coverage check) for each equation, and another pairwise check is used only when i /= j. The Algorithm U stuff stays, but *without equation 7*. The proof would have to be tweaked, but I think this will give us a full proof of soundness. (Yay!) And it will all be easier to extend to generalized injectivity annotations.
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> So, I agree with Simon's proposal: explain all of this in terms of two separate checks. One check does a coverage check (very like the FD coverage check) for each equation, and another pairwise check is used only when i /= j. The Algorithm U stuff stays, but \*without equation 7\*. The proof would have to be tweaked, but I think this will give us a full proof of soundness. (Yay!) And it will all be easier to extend to generalized injectivity annotations.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
### Inferring injectivity
|
|
|
|
... | ... | @@ -924,7 +579,7 @@ type family F a b c ... n = r where |
|
|
```
|
|
|
|
|
|
|
|
|
Since there are n arguments there are 2<sup>n possible injectivity annotations.
|
|
|
Since there are n arguments there are 2<sup>n</sup> possible injectivity annotations.
|
|
|
That's why I believed that we have to check every possible annotationton. I now
|
|
|
believe that instead checking every possible annotation we should only check
|
|
|
whether knowing the RHS allows to infer each argument independently. In other
|
... | ... | @@ -932,7 +587,6 @@ words when inferring injectivity we would check whether annotations `r -> a`, \` |
|
|
-\> b`, `r -\> c` ... `r -\> n` hold true. If we learn for example that knowing `r\`
|
|
|
allows to infer `a`, `c` and `n` but not the other argumenst we infer the
|
|
|
annotation `r -> a c n`.
|
|
|
</sup>
|
|
|
|
|
|
|
|
|
There are several concerns to consider before implementing this:
|
... | ... | |