October 2014 - ghc-tickets

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:76 simonpj]: > * My brain is too small to think about verifying injectivity for closed families. Richard? I've put some comments on the wiki page. But the whole thing makes me a little nervous, as closed type families are really squirrelly. I would want something resembling a proof before feeling truly confident. As a first pass, we could always treat the equations of a closed family as independent (like an open family). I believe that such a treatment would be fully conservative. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:81> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:75 jstolarek]: > Good question. I have not considered such case earlier. Here are some thoughts: > > Currently your `Map` function will work only for type constructors because unsaturated type families are not allowed. These are certainly injective. > > First step in my current outline of the algorithm that decides whether a type family is injective or not says: "If a RHS contains a call to a type family we conclude that the type family is not injective. I am not certain if this extends to self-recursion -- see discussion below." This would lead to conclusion that `Map` is not injective because `Map` calls itself. > > Now let's say I manage to find a way to allow self-recursion (see discussion on the wiki page). I'm left with the problematic call to `f`. As stated earlier currently this must be an injective type constructor. So it seems that declaring `Map` injective should be safe because type constructors are generative and it seems possible to deduce `f`, `a` and `b` from `Map f [a, b] ~ [Maybe Int, Maybe Char]`. At the moment I have no idea how to formulate an algorithm for such a deduction. Could this be done by the current constraint solver? This should just work with the algorithm already stated. (Except for the self-recursion bit, which I responded to on the wiki page.) Unification should do the work for you. > > What if we were allowed to have partially applied type families (say, because we've implemented ideas from singletons) and `f` could be a type family? Would knowing that `f` is injective allow us to declare `Map` as injective? Injectivity says you can deduce LHS from RHS but I think that it would not be a good idea to try to solve `Map f [a, b] ~ [Int, Char]`. And so the restriction on not having calls to type families on the RHS would rightly declare `Map` as not injective. So if we had partially applied type families and thus `f` was allowed to be either a type constructor a type family we should declare `Map` as not injective. This contrasts with earlier paragraph, where knowing that `f` must be a type constructor allowed us to declare `Map` as injective. > > Does that make sense? No. Under the singletons work, we gave a different kind to non-injective functions, so Gabor's kind -- using `->`, not any other arrow -- requires an injective argument. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:80> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:73 jstolarek]: > 2. That condition must contain only the result type variable on the LHS of `->` and all other type variables on the RHS of `->`. In other words if I declare `type family P a b = r` then I'm only allowed to write `r -> a b` or `r -> b a` injectivity condition. Questions here: a) can I add a restriction that type variables on the RHS must be given in exactly the same order as they were given in the head declaration? This would make the implementation simpler; b) where should this check be done? In the renamer? I'm ambivalent on this design decision (that the variables have to be in the same order in the annotation). I suppose it simplifies the implementation. Yes, the renamer seems like a fine-enough place to do the check. > > 3. Once we check 2) we must verify that the type family is indeed injective. Not sure where this should happen? My guess is that during typechecking of a type family equations. Algorithm is outlined [wiki:InjectiveTypeFamilies#Implementationoutline here]. Please see updates to the wiki page, labeled '''RAE''' ... '''End RAE'''. > > Does the implementation plan outlined so far look sensible? Are there any misconceptions? > > 4. Once we pass these checks injectivity becomes a binary property, so we can discard injectivity conditions written by the user and replace it with a `Bool`. Richard, when we first spoke about injective type families you suggested that all the magic will go into `isDecomposableTyCon` in `types/TyCon.lhs`. I've added a `Bool` field to `SynTyCon` data constructor of `TyCon` data type and made `isDecomposableTyCon` use that field to tell whether a type family is injective or not. (Checks described in 2 and 3 are not implemented. When a user writes injectivity declaration for a type family I just assume it is correct.) Sadly, this does not work. Here's an example test case: > > {{{#!hs > type family F a = r | r -> a where > F Int = Bool > F Bool = Int > F a = a > > foo :: F a -> F a > foo = id > }}} > > This fails with: > > {{{ > Couldn't match type ‘F a0’ with ‘F a’ > NB: ‘F’ is a type function, and may not be injective > The type variable ‘a0’ is ambiguous > Expected type: F a -> F a > Actual type: F a0 -> F a0 > In the ambiguity check for: forall a. F a -> F a > To defer the ambiguity check to use sites, enable AllowAmbiguousTypes > In the type signature for ‘foo’: foo :: F a -> F a > }}} > > I added traces to verify that `isDecomposableTyCon` is called for `F` type family and it correctly returns `True`. > > Out of curiosity I turned on `AllowAmbiguousTypes` and added a definition like this: > > {{{ > bar :: Int -> Int > bar = foo > }}} > > That failed with: > > {{{ > Couldn't match type ‘F a0’ with ‘Int’ > The type variable ‘a0’ is ambiguous > Expected type: Int -> Int > Actual type: F a0 -> F a0 > In the expression: foo > In an equation for ‘bar’: bar = foo > }}} > > I imagine that getting this one to work definitely requires more changes than just `isDecomposableTyCon`. Yes, Simon's comment above is correct -- I was just wrong about the `isDecomposableTyCon` thing. Actually, injective type families still need to say "no" to `isDecomposableTyCon`, because of the '''left''' and '''right''' coercion formers, which assume generativity. > Then again GHC can already deal with some cases of injectivity: > > {{{#!hs > type family F a = r | r -> a where > F Int = Int > F Bool = Bool > F a = a > > foo :: F a -> F a > foo = id > > bar :: Int -> Int > bar = foo > }}} > > That works perfectly fine in GHC 7.8. What works perfectly fine? Not the code you wrote above, because it contains a not-currently-parsed injectivity annotation. I tried it without the injectivity annotation, and it does indeed work. But not because of injectivity, at all: it's because GHC is clever enough to figure out that `F` is just an identity function, and so the `F a`s in `foo`'s type become `a`. If you swap the `Int` and `Bool` RHSs in the definition (which preserves injectivity), the code fails to compile. > > I tried to analyse what's going on with `-ddump-tc-trace` but the dumps are 600-1000 lines long. Of course the source code itself is even longer, so I'd appreciate any directions where should I start looking. Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :) > > One final question. Assuming that `SynTyCon` really should have a new field, I believe this field should be stored in interface files. After all we want injectivity information to propagate from one module to another. Now I wonder how this interacts with open type families. I understand that these are typechecked progressively as we find more equations. I haven't looked at the implementation but my intuition from reading GHC papers is that in a given module we import open type family equations from other modules, collect equations from current module and proceed with type checking of an open type family. Is that intuition correct? If so then I believe that checking of injectivity (point 3 of my outline) should be done during this stage (I believe it would be best to combine it with checking equation overlapping). Agreed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:79> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by simonpj): Yes "Wanted" and "Derived". You'll see lots of this with `-ddump-tc- trace` -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:78> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Replying to [comment:76 simonpj]: > * We are not (at least for now) changing System FC. So the only effect of injectivity is to add extra "Derived" unification constraints, very much like functional dependencies. If we see > {{{ > [W] F t ~ F s > }}} > then we don't decopose it. Instead we add > {{{ > [D] t ~ s > }}} What is the meaning of `[W]` and `[D]`? "Wanted" and "derived"? > * I don't understand the discussion of `Map`. Are you perhaps discussing how to verify some (not shown here) implementation of a closed type family `Map` is in fact injective? Yes, I was discussing how to verify whether this definition of `Map` is injective: {{{#!hs type family Map (f :: k -> l) (ks :: [k]) :: [l] where Map f '[] = '[] Map f (x ': xs) = f x ': Map f xs }}} > * Verifying injectivity for open families: if the RHSs unify then the LHSs should be identical under that substitution. Eg > {{{ > type instance F a Int = a -> Int > type instance F Int a = Int -> a > }}} > These are consistent (and hence allowed) and are injective in both arguments. Ah, I haven't thought about allowing substitution when RHSs unify. Wiki updated. > * My brain is too small to think about verifying injectivity for closed families. Richard? I only remind that I outlined an algorithm on the wiki :-) Richard, it would be great if you could take a look and say whether it makes sense. In the meantime I have almost implemented checking correctness of injectivity condition (point 2 from [comment:73 my earlier comment]). Renamer seems to be the right place for doing this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:77> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by simonpj): * I think it's very straightforward to allow injectivity of form `r -> <subset of args>`. That is, the rhs is unconstrained but the lhs must be `r`. * So injectivity isn't a binary property; rather it's a `Bool` per argument. Making this list a field of `SynTyCon` is probably right, with ordinary synonyms being all false. * We are not (at least for now) changing System FC. So the only effect of injectivity is to add extra "Derived" unification constraints, very much like functional dependencies. If we see {{{ [W] F t ~ F s }}} then we don't decopose it. Instead we add {{{ [D] t ~ s }}} That guides inference, but does not produce proof terms. So, no, nothing to do with `isDecomposableTyCon`. Much more like the `try_improvement` code in `TcInteract.doTopReactFunEq`. * I don't understand the discussion of `Map`. Are you perhaps discussing how to verify some (not shown here) implementation of a closed type family `Map` is in fact injective? * Verifying injectivity for open families: if the RHSs unify then the LHSs should be identical under that substitution. Eg {{{ type instance F a Int = a -> Int type instance F Int a = Int -> a }}} These are consistent (and hence allowed) and are injective in both arguments. * My brain is too small to think about verifying injectivity for closed families. Richard? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:76> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Good question. I have not considered such case earlier. Here are some thoughts: Currently your `Map` function will work only for type constructors because unsaturated type families are not allowed. These are certainly injective. First step in my current outline of the algorithm that decides whether a type family is injective or not says: "If a RHS contains a call to a type family we conclude that the type family is not injective. I am not certain if this extends to self-recursion -- see discussion below." This would lead to conclusion that `Map` is not injective because `Map` calls itself. Now let's say I manage to find a way to allow self-recursion (see discussion on the wiki page). I'm left with the problematic call to `f`. As stated earlier currently this must be an injective type constructor. So it seems that declaring `Map` injective should be safe because type constructors are generative and it seems possible to deduce `f`, `a` and `b` from `Map f [a, b] ~ [Maybe Int, Maybe Char]`. At the moment I have no idea how to formulate an algorithm for such a deduction. Could this be done by the current constraint solver? What if we were allowed to have partially applied type families (say, because we've implemented ideas from singletons) and `f` could be a type family? Would knowing that `f` is injective allow us to declare `Map` as injective? Injectivity says you can deduce LHS from RHS but I think that it would not be a good idea to try to solve `Map f [a, b] ~ [Int, Char]`. And so the restriction on not having calls to type families on the RHS would rightly declare `Map` as not injective. So if we had partially applied type families and thus `f` was allowed to be either a type constructor a type family we should declare `Map` as not injective. This contrasts with earlier paragraph, where knowing that `f` must be a type constructor allowed us to declare `Map` as injective. Does that make sense? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:75> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by heisenbug): Replying to [comment:73 jstolarek]: > Simon, Richard, others, > > I'm making progress on this one but before going too far I want to get a green light on my design proposal (points 1-3). I've also bumped into some problems and have a couple of questions. > Just a side question. I have a type level Map: {{{ type family Map (f :: k -> l) (ks :: [k]) :: [l] where ... }}} When I declare this as injective (presumably) with {{{ type family Map (f :: k -> l) (ks :: [k]) = result :: [l] | result -> ks where ... }}} then `f` must be injective for this to work. Concretely, will this invocation be considered injective by GHC (`:set -XDataKinds`) ? {{{ Map IO '[Int, (), Bool] }}} Thanks, Gabor -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:74> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Oct '14

10 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Simon, Richard, others, I'm making progress on this one but before going too far I want to get a green light on my design proposal (points 1-3). I've also bumped into some problems and have a couple of questions. My design proposal is to implement only injectivity of type A (ie. plain injectivity in all arguments). The consequences of this are: 1. A user is allowed to write at most one injectivity condition. 2. That condition must contain only the result type variable on the LHS of `->` and all other type variables on the RHS of `->`. In other words if I declare `type family P a b = r` then I'm only allowed to write `r -> a b` or `r -> b a` injectivity condition. Questions here: a) can I add a restriction that type variables on the RHS must be given in exactly the same order as they were given in the head declaration? This would make the implementation simpler; b) where should this check be done? In the renamer? 3. Once we check 2) we must verify that the type family is indeed injective. Not sure where this should happen? My guess is that during typechecking of a type family equations. Algorithm is outlined [wiki:InjectiveTypeFamilies#Implementationoutline here]. Does the implementation plan outlined so far look sensible? Are there any misconceptions? 4. Once we pass these checks injectivity becomes a binary property, so we can discard injectivity conditions written by the user and replace it with a `Bool`. Richard, when we first spoke about injective type families you suggested that all the magic will go into `isDecomposableTyCon` in `types/TyCon.lhs`. I've added a `Bool` field to `SynTyCon` data constructor of `TyCon` data type and made `isDecomposableTyCon` use that field to tell whether a type family is injective or not. (Checks described in 2 and 3 are not implemented. When a user writes injectivity declaration for a type family I just assume it is correct.) Sadly, this does not work. Here's an example test case: {{{#!hs type family F a = r | r -> a where F Int = Bool F Bool = Int F a = a foo :: F a -> F a foo = id }}} This fails with: {{{ Couldn't match type ‘F a0’ with ‘F a’ NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: F a -> F a Actual type: F a0 -> F a0 In the ambiguity check for: forall a. F a -> F a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘foo’: foo :: F a -> F a }}} I added traces to verify that `isDecomposableTyCon` is called for `F` type family and it correctly returns `True`. Out of curiosity I turned on `AllowAmbiguousTypes` and added a definition like this: {{{ bar :: Int -> Int bar = foo }}} That failed with: {{{ Couldn't match type ‘F a0’ with ‘Int’ The type variable ‘a0’ is ambiguous Expected type: Int -> Int Actual type: F a0 -> F a0 In the expression: foo In an equation for ‘bar’: bar = foo }}} I imagine that getting this one to work definitely requires more changes than just `isDecomposableTyCon`. Then again GHC can already deal with some cases of injectivity: {{{#!hs type family F a = r | r -> a where F Int = Int F Bool = Bool F a = a foo :: F a -> F a foo = id bar :: Int -> Int bar = foo }}} That works perfectly fine in GHC 7.8. I tried to analyse what's going on with `-ddump-tc-trace` but the dumps are 600-1000 lines long. Of course the source code itself is even longer, so I'd appreciate any directions where should I start looking. One final question. Assuming that `SynTyCon` really should have a new field, I believe this field should be stored in interface files. After all we want injectivity information to propagate from one module to another. Now I wonder how this interacts with open type families. I understand that these are typechecked progressively as we find more equations. I haven't looked at the implementation but my intuition from reading GHC papers is that in a given module we import open type family equations from other modules, collect equations from current module and proceed with type checking of an open type family. Is that intuition correct? If so then I believe that checking of injectivity (point 3 of my outline) should be done during this stage (I believe it would be best to combine it with checking equation overlapping). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:73> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7473: getModificationTime gives only second-level resolution
by GHC 10 Oct '14

10 Oct '14

#7473: getModificationTime gives only second-level resolution -------------------------------------+------------------------------------- Reporter: duncan | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.6.1 Libraries | Keywords: directory Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by ekmett): We should be able to make that happen. We'll need to reach out to Bryan O'Sullivan to get the version bump done; Win32 isn't under core libraries control. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7473#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0