September 2014 - ghc-tickets

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:59 goldfire]: > plain old injectivity for open type families. > more involved reasoning for closed type families, where inference is possible I'm not sure what design choices are hidden by these two statements. Do you mean that for open type families we would have: a) simple injectivity in the result only (via annotations) or b) injectivity in some of the arguments (also via annotations); whereas for closed type families we would admit the same kind of injectivity declarations as for open type families and perhaps also injectivity inference as proposed by me in comment 58? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:61> 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 heisenbug): Replying to [comment:58 jstolarek]: > Replying to [comment:56 heisenbug]: > > Tim Sheard has a nice 2006 paper on how to do it. > > What's the title of this paper? I tried to google it but failed. > "Type-level Computation Using Narrowing in Ωmega", Elsevier, 2007 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:60> 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): Simon's (very straightforward) example clarifies this in my mind -- I agree about just heading for plain old injectivity for open type families. If/when we want more involved reasoning for closed type families, where inference is possible, we can address that. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:59> 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:56 heisenbug]: > Tim Sheard has a nice 2006 paper on how to do it. What's the title of this paper? I tried to google it but failed. Replying to [comment:45 simonpj]: > For closed type classes, can't we infer injectivity, rather than having to declare it? I thought about it and I believe this should be possible. But we could only infer normal injectivity. I believe an algorithm for inferring injectivity in some of the parameters (ie. things like `result a -> b c` or `result -> b c` for a 3-arity type family) would be exponential in the number of arguments. Inferring normal injectivity should be O(n^2^) at most, where n is the number of equations. Replying to [comment:57 simonpj]: > But we have no actual use-caes for anything except Number 1 Goal, for equalities of form `F t1 ~ F t2`. It looks like Conal Elliot has a use case for injectivity in only some arguments: http://www.haskell.org/pipermail/glasgow-haskell- users/2011-February/020027.html I'll contact him for more details. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:58> 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 simonpj): (GHC does, in effect, use narrowing, I believe.) Let's stand back a bit. What are we trying to achieve. Here is the Number 1 Goal: if the type inference engine is trying to prove `F a ~ F beta`, where `a` is a skolem constant and `beta` is a unification variable, is it justified in fixing `beta := a`? If `F` is not injective the answer is "no". If it's injective, the answer is "yes". We have multiple examples of the need for this. More generally, our goal is to use injectivity to guide the decision about what type a unification varaible stands for. Injectivity also allows other such opportunities, beyond the Number 1 Goal above. Suppose `F` is injective, and we have {{{ F Int = True }}} Then if we have `F beta ~ True` we can deduce `beta := Int`. Richard raises further possiblities: possibly-partial information about the result might allow us to deduce possibly-partial information about the arguments. That is the stuff about head-injectivity and it seems to be potentially very complicated. Take a closed type family. If I tell you something (but perhaps not everything) about the result, perhaps you can tell me something (but perhaps not everything) about the argument. I don't know how clever you might be here, or how to declare the cleverness in an "injectivity signature" for open families. But we have no actual use-caes for anything except Number 1 Goal, for equalities of form `F t1 ~ F t2`. It seems that equalities of form `F t1 ~ some-type` offer potential opportunities, but I don't see a sweet spot. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:57> 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 10 Sep '14

10 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: 9421 | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by cetu86): This did it. Thank you! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:17> 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 heisenbug): Replying to [comment:48 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". > So when our goal is to make progress from the target expression towards the source expression, what hinders us to follow Omega and use narrowing to obtain the head? Tim Sheard has a nice 2006 paper on how to do it. It is really powerful and we could insist that exactly one solution exists. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:56> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #9570: cryptarithm1 (normal) has bimodal runtime
by GHC 10 Sep '14

10 Sep '14

#9570: cryptarithm1 (normal) has bimodal runtime -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: NoFib benchmark | Version: 7.9 suite | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Difficulty: Unknown | None/Unknown Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- I was investigating performance numbers for cryptarithm1 in #8199, I noticed that the numbers for this benchmark were curiously bimodal. Here are two representative samples from both sides of the distribution. {{{ ../../runstdtest/runstdtest ./cryptarithm1 -o1 cryptarithm1.stdout -o1 cryptarithm1.stdout -ghc-timing ; ../../runstdtest/runstdtest ./cryptarithm1 -o1 cryptarithm1.stdout -o1 cryptarithm1.stdout -ghc- timing ; ../../runstdtest/runstdtest ./cryptarithm1 -o1 cryptarithm1.stdout -o1 cryptarithm1.stdout -ghc-timing ; ../../runstdtest/runstdtest ./cryptarithm1 -o1 cryptarithm1.stdout -o1 cryptarithm1.stdout -ghc-timing ; ../../runstdtest/runstdtest ./cryptarithm1 -o1 cryptarithm1.stdout -o1 cryptarithm1.stdout -ghc- timing ; real 0m0.676s user 0m0.660s sys 0m0.013s <<ghc: 2051819320 bytes, 3929 GCs (3927 + 2), 0/0 avg/max bytes residency (0 samples), 5221368 bytes GC work, 1M in use, 0.000 INIT (0.000 elapsed), 0.643 MUT (0.643 elapsed), 0.026 GC (0.026 elapsed), 0.026 GC(0) (0.025 elapsed), 0.000 GC(1) (0.000 elapsed), 1 balance :ghc>> real 0m0.610s user 0m0.603s sys 0m0.007s <<ghc: 2051819320 bytes, 3929 GCs (3927 + 2), 0/0 avg/max bytes residency (0 samples), 5221368 bytes GC work, 1M in use, 0.000 INIT (0.000 elapsed), 0.582 MUT (0.582 elapsed), 0.023 GC (0.023 elapsed), 0.023 GC(0) (0.023 elapsed), 0.000 GC(1) (0.000 elapsed), 1 balance :ghc>> }}} I don't have any further resolution on the problem yet. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9570> 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: 9421 | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by rwbarton): It does. Probably you have gotten your non-submodule subrepositories into an inconsistent state, something which is easy to do when checking out 7.8. The reliable way to check out 7.8 correctly is to start with a fresh clone: {{{ git clone -b ghc-7.8 git://git.haskell.org/ghc.git cd ghc ./sync-all get -b ghc-7.8 }}} Sorry the wiki can be unclear in places... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:16> 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: 9421 | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by cetu86): Thanks again, for the reply. :-) Don't know why I thought passing "quick-perf" as an argument to make would choose the flavor. I now did as you said, created a build.mk from build.mk.sample and set {{{ BuildFlavour = quick-cross }}} which pulls in {{{ INTEGER_LIBRARY = integer-simple }}} I only need the simple cross-compiler (at the moment). Now I come as far as {{{ "inplace/bin/ghc-stage1" -hisuf hi -osuf o -hcsuf hc -static -H64m -O0 -package-name ghc-7.8.3 -hide-all-packages -i -icompiler/basicTypes -icompiler/cmm -icompiler/codeGen -icompiler/coreSyn -icompiler/deSugar -icompiler/ghci -icompiler/hsSyn -icompiler/iface -icompiler/llvmGen -icompiler/main -icompiler/nativeGen -icompiler/parser -icompiler/prelude -icompiler/profiling -icompiler/rename -icompiler/simplCore -icompiler/simplStg -icompiler/specialise -icompiler/stgSyn -icompiler/stranal -icompiler/typecheck -icompiler/types -icompiler/utils -icompiler/vectorise -icompiler/stage2/build -icompiler/stage2/build/autogen -Icompiler/stage2/build -Icompiler/stage2/build/autogen -Icompiler/. -Icompiler/parser -Icompiler/utils -Icompiler/../rts/dist/build -Icompiler/stage2 -optP- DGHCI -optP-include -optPcompiler/stage2/build/autogen/cabal_macros.h -package Cabal-1.18.1.3 -package array-0.5.0.1 -package base-4.7.0.0 -package bin-package-db-0.0.0.0 -package bytestring-0.10.4.0 -package containers-0.5.5.1 -package directory-1.2.1.0 -package filepath-1.3.0.2 -package hoopl-3.10.0.1 -package hpc-0.6.0.1 -package process-1.2.0.0 -package template-haskell-2.10.0.0 -package time-1.4.2 -package transformers-0.3.0.0 -package unix-2.7.0.2 -Wall -fno-warn-name-shadowing -XHaskell98 -XCPP -XMagicHash -XUnboxedTuples -XPatternGuards -XForeignFunctionInterface -XEmptyDataDecls -XTypeSynonymInstances -XMultiParamTypeClasses -XFlexibleInstances -XRankNTypes -XScopedTypeVariables -XDeriveDataTypeable -XBangPatterns -XNondecreasingIndentation -DNO_REGS -DNOSMP -optc-DNOSMP -optc- DTHREADED_RTS -DSTAGE=2 -O0 -fllvm -no-user-package-db -rtsopts -odir compiler/stage2/build -hidir compiler/stage2/build -stubdir compiler/stage2/build -c compiler/hsSyn/Convert.lhs -o compiler/stage2/build/Convert.o compiler/hsSyn/Convert.lhs:895:10: Not in scope: data constructor ‘TH.ClassP’ Perhaps you meant one of these: ‘TH.ClassD’ (imported from Language.Haskell.TH.Syntax), ‘TH.ClassD’ (imported from Language.Haskell.TH), ‘TH.ClassI’ (imported from Language.Haskell.TH.Syntax) compiler/hsSyn/Convert.lhs:900:10: Not in scope: data constructor ‘TH.EqualP’ make[1]: *** [compiler/stage2/build/Convert.o] Error 1 make: *** [all] Error 2 }}} TH stands for template haskell, right? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0