- ghc-tickets - Haskell.org

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:53 jstolarek]: > Also, if I understood correctly it is possible to have both injectivity and head-injectivity in the compiler, right? Yes, but confusing, especially if there is syntax for both. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:55> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): Replying to [comment:51 goldfire]: > Replying to [comment:49 jstolarek]: > > I don't think that restricting the use of `result` word in type family head is a big problem - we've already done that with `role`. > > The use of `role` doesn't steal syntax: it can be used only after the word `type` in a top-level declaration, where a capitalized identifier is expected. Oops, sorry for defamation then ;-) Still, I think that the price to pay for using `result` will not be that high. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:54> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): Replying to [comment:52 goldfire]: > Here, "head" means the head of the RHS type, not the type declaration -- it's the root of the type's AST. Does that help? Yes, now I fully understand. Also, if I understood correctly it is possible to have both injectivity and head-injectivity in the compiler, right? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:53> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:50 jstolarek]: > Could you explain what you mean by `RHSs with different heads` and `below the heads`? Up till now I thought that the term "head" refers to `type family F a` part of the declaration. Here, "head" means the head of the RHS type, not the type declaration -- it's the root of the type's AST. Does that help? > > I also don't understand why `G` is not head-injective, but perhaps this will become clear to me once earlier questions are answered. `G` isn't head-injective because both RHSs are headed by `Just`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:52> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:49 jstolarek]: > I don't think that restricting the use of `result` word in type family head is a big problem - we've already done that with `role`. The use of `role` doesn't steal syntax: it can be used only after the word `type` in a top-level declaration, where a capitalized identifier is expected. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:51> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

10 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): Richard, I don't understand your terminology here (though I do understand the `F` example): > The equations defining a head-injective function all have RHSs with different heads. What appears below the heads does not matter. Could you explain what you mean by `RHSs with different heads` and `below the heads`? Up till now I thought that the term "head" refers to `type family F a` part of the declaration. I also don't understand why `G` is not head-injective, but perhaps this will become clear to me once earlier questions are answered. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:50> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 09 Sep '14

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): I think the bulk of the work with injectivity will be done under the hood. Changing the syntax later on will not be difficult and I don't want to be blocked by bikeshedding. Inferring injectivity for closed type families is something that indeed requires more discussion. But again, I feel I can make at least some progress without any binding decissions on this matter being made. I don't like any of Richard's proposals: - if we introduced `Result` this would be the first capitalized keyword (reserved word?) in Haskell. I don't like such inconsistency. Notice also that `result` might conflict with type variable names in type family head but that is a local conflict that restricts only the names possible to use for type variables. On the other hand `Result` might conflict with a name of a type (or type family), which is more of a global thing. - if we use syntax that uses type family name then we will get something like `type family F a b c | F b -> a c` and `F b` looks strange given that `F`'s arity is 3. It looks as if `F` could be partially applied. I don't think that restricting the use of `result` word in type family head is a big problem - we've already done that with `role`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:49> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 09 Sep '14

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): A conversation with Ulf Norell (the first implementor of Agda) led to this interesting thought: We may not want injectivity -- we may want a weaker property, which I'll term "head-injectivity". The equations defining a head-injective function all have RHSs with different heads. What appears below the heads does not matter. Here is an example: {{{#!hs type family F a where F (Just x) = True F Nothing = False }}} This function is ''not'' injective: `F (Just 1) ~ F (Just 2)`. Yet, it is head-injective. If the type-inferencer knows that `F x ~ True`, it can then refine `x ~ Just y` for some fresh unification variable `y`. This improvement may be enough to make further progress. Of course, injectivity does not imply head-injectivity. Consider {{{#!hs type family G a where G True = Just 1 G False = Just 2 }}} This function is injective but not head-injective. So, implementing only head-injectivity will miss this case. But, perhaps we can refine the notion of head-injectivity simply to mean that the RHSs don't unify. The reason I'm bringing this up is that head-injectivity is, as I understand it, implemented in Agda and used during type inference. It intrigues me to think that we can make progress in the case of `F`, a non- injective function. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:48> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6086: Cross compilation fails using system linker for other architecture binaries
by GHC 09 Sep '14

09 Sep '14

#6086: Cross compilation fails using system linker for other architecture binaries ----------------------------------------------+--------------------------- Reporter: mtjm | Owner: Type: bug | Status: new Priority: high | Milestone: 7.8.4 Component: Build System | Version: 7.8.3 Resolution: | Keywords: Operating System: Linux | Architecture: arm Type of failure: Building GHC failed | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by rwbarton): Try adding `--with-gcc=[whatever the path to the C cross-compiler is]` to the configure command line. I've found that I need to do this when cross- compiling. I think that configure detecting the C cross-compiler worked in 7.8.2 and broke in 7.8.3 but I'm not 100% sure. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 09 Sep '14

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by rwbarton): We could also reuse an existing keyword, e.g., `type family F a :: * | type -> a`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:47> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0