RE: Trying to build Agda 2.2.9 with ghc-7.1.20110131
Pavel Concerning Another one, the problem is that with BangPatterns enabled, GHC understands vs ! i = ... to mean vs (!i) = ... with a bang-pattern, thus defining vs rather than (!). Reason: the common case of saying f !x !y = e is so convenient that we didn't want to require parens. But the cost is that you can't define (!) in an infix way. So that's that one. For the profiling thing, is this the same as http://hackage.haskell.org/trac/ghc/ticket/4462? What happens if you say -dcore-lint?We should look at #4462. Simon From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Pavel Perikov Sent: 01 February 2011 15:01 To: GHC users Subject: Trying to build Agda 2.2.9 with ghc-7.1.20110131 If anyone interested... Agda-2.2.9 compiled perfectly with 7.0.1 release but with 7.1.20110131 the compiler had a few problems including impossible happened when building profiling library. Another one was in src/full/Agda/TypeChecking/Positivity.hs @ 260: instance ComputeOccurrences Term where occurrences vars v = case v of Var i args - maybe Map.empty here (vars ! fromIntegral i) .. where vs ! i | i length vs = vs !! i | otherwise = error $ show vs ++ ! ++ show i ++ ( ++ show v ++ ) Compiler complained about ! in vars ! fromIntegral suggesting Map.! after i changed the code to where (!) vs i | i length vs = vs !! i | otherwise = error $ show vs ++ ! ++ show i ++ ( ++ show v ++ ) everything proceeded as expected. I also had to give -XFlexibleInstances and -XBangPatterns that was not required previously. Agda can be got from darcs get http://code.haskell.org/Agda/ pavel. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Injective type families?
Is there a way to declare a type family to be injective? I have data Z data S n type family n :+: m type instance Z :+: m = m type instance S n :+: m = S (n :+: m) My intent is that (:+:) really is injective in each argument (holding the other as fixed), but I don't know how to persuade GHC, leading to some compilation errors like the following: Couldn't match expected type `m :+: n' against inferred type `m :+: n1' NB: `:+:' is a type function, and may not be injective I realize that someone could add more type instances for (:+:), breaking injectivity. Come to think of it, I don't know how GHC could even figure out that the two instances above do not overlap on the right-hand sides. Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue? Thanks, - Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Injective type families?
Isn't this what data families (as opposed to type families) do? John On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott co...@conal.net wrote: Is there a way to declare a type family to be injective? I have data Z data S n type family n :+: m type instance Z :+: m = m type instance S n :+: m = S (n :+: m) My intent is that (:+:) really is injective in each argument (holding the other as fixed), but I don't know how to persuade GHC, leading to some compilation errors like the following: Couldn't match expected type `m :+: n' against inferred type `m :+: n1' NB: `:+:' is a type function, and may not be injective I realize that someone could add more type instances for (:+:), breaking injectivity. Come to think of it, I don't know how GHC could even figure out that the two instances above do not overlap on the right-hand sides. Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue? Thanks, - Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Injective type families?
Yes, it's one things that data families do. Another is introducing *new* data types rather than reusing existing ones. - Conal On Mon, Feb 14, 2011 at 1:41 PM, John Meacham j...@repetae.net wrote: Isn't this what data families (as opposed to type families) do? John On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott co...@conal.net wrote: Is there a way to declare a type family to be injective? I have data Z data S n type family n :+: m type instance Z :+: m = m type instance S n :+: m = S (n :+: m) My intent is that (:+:) really is injective in each argument (holding the other as fixed), but I don't know how to persuade GHC, leading to some compilation errors like the following: Couldn't match expected type `m :+: n' against inferred type `m :+: n1' NB: `:+:' is a type function, and may not be injective I realize that someone could add more type instances for (:+:), breaking injectivity. Come to think of it, I don't know how GHC could even figure out that the two instances above do not overlap on the right-hand sides. Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue? Thanks, - Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Injective type families?
I think what you want is closed type families, as do I and many others :) Unfortunately we don't have those. On Mon, Feb 14, 2011 at 10:02 PM, Conal Elliott co...@conal.net wrote: Yes, it's one things that data families do. Another is introducing *new* data types rather than reusing existing ones. - Conal On Mon, Feb 14, 2011 at 1:41 PM, John Meacham j...@repetae.net wrote: Isn't this what data families (as opposed to type families) do? John On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott co...@conal.net wrote: Is there a way to declare a type family to be injective? I have data Z data S n type family n :+: m type instance Z :+: m = m type instance S n :+: m = S (n :+: m) My intent is that (:+:) really is injective in each argument (holding the other as fixed), but I don't know how to persuade GHC, leading to some compilation errors like the following: Couldn't match expected type `m :+: n' against inferred type `m :+: n1' NB: `:+:' is a type function, and may not be injective I realize that someone could add more type instances for (:+:), breaking injectivity. Come to think of it, I don't know how GHC could even figure out that the two instances above do not overlap on the right-hand sides. Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue? Thanks, - Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Injective type families?
On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote: I think what you want is closed type families, as do I and many others :) Unfortunately we don't have those. Closed type families wouldn't necessarily be injective, either. What he wants is the facility to prove (or assert) to the compiler that a particualr type family is in fact injective. It's something that I haven't really even seen developed much in fancy dependently typed languages, though I've seen the idea before. That is: prove things about your program and have the compiler take advantage of it. -- Dan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Injective type families?
Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be: * You declare the family to be injective injective type family T a :: * * At every type instance, injectivity is checked. That is, if you say type instance T (a,Int) = Either a Bool then we must check that every type instance whose LHS unifies with this has the same RHS under the unifying substitution. Thus type instance T (a,Bool) = [a] -- OK; does not unify type instance T (Int,b) = Either Int Bool -- OK; same RHS on (Int,Int) I think it's mainly a question of tiresome design questions (notably do we want a new keyword injective? Should it go before type?) and hacking to get it all implemented. Simon | -Original Message- | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Dan Doel | Sent: 14 February 2011 23:14 | To: glasgow-haskell-users@haskell.org | Subject: Re: Injective type families? | | On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote: | I think what you want is closed type families, as do I and many others :) | Unfortunately we don't have those. | | Closed type families wouldn't necessarily be injective, either. What he wants | is the facility to prove (or assert) to the compiler that a particualr type | family is in fact injective. | | It's something that I haven't really even seen developed much in fancy | dependently typed languages, though I've seen the idea before. That is: prove | things about your program and have the compiler take advantage of it. | | -- Dan | | ___ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Injective type families?
On Mon, Feb 14, 2011 at 1:41 PM, John Meacham j...@repetae.net wrote: Isn't this what data families (as opposed to type families) do? On Tue, Feb 15, 2011 at 7:02 AM, Conal Elliott co...@conal.net wrote: Yes, it's one things that data families do. Another is introducing *new* data types rather than reusing existing ones. - Conal Roman Leshchinskiy once used a newtype to make a type family injective and remarked: As an aside, it is well possible to [use] an injective data type family or even a GADT [instead]. ... However, this really messes up GHC’s optimiser and leads to very inefficient code. [1] Of course, introducing a newtype also requires introducing new types instead of reusing existing ones.. Sebastian [1]: http://unlines.wordpress.com/2010/11/15/generics-for-small-fixed-size-vectors/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
