Re: [Haskell-cafe] Re: Optimization problem
On Tue, Sep 19, 2006 at 01:52:02PM +0100, Conor McBride wrote: [EMAIL PROTECTED] wrote: Btw, why are there no irrefutable patterns for GADTs? Just imagine data Eq a b where Refl :: Eq a a coerce :: Eq a b - a - b coerce ~Refl a = a coerce undefined True :: String Bang you're dead. Or rather... Twiddle you're dead. Does anything go wrong with irrefutable patterns for existential types? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: Optimization problem
| Does anything go wrong with irrefutable patterns for existential types? Try giving the translation into System F. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Thu, Sep 28, 2006 at 03:22:25PM +0100, Simon Peyton-Jones wrote: | Does anything go wrong with irrefutable patterns for existential types? Try giving the translation into System F. Hmm, that's not quite as satisfying as Conor's answer for GADTs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Tue, Sep 19, 2006 at 08:06:07PM +0200, [EMAIL PROTECTED] wrote: For our optimization problem, it's only a matter of constructors on the right hand side. They should pop out before do not look on any arguments, so it's safe to cry so you just know, i'm a Just. It seems the appropriate encoding would be for the shape to be an inductive datatype and the contents (as well as the lists) to be coinductive, as access to the contents is gated through the shape. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Tue, Sep 19, 2006 at 01:41:51PM +0200, [EMAIL PROTECTED] wrote: Btw, why are there no irrefutable patterns for GADTs? Not GADTs, but existential types (whether done with GADTs or not). They can't be analysed with irrefutable patterns, of which let bindings are a special case: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html#id3143545 See the second restriction. Irrefutable patterns aren't mentioned there, but they're the general case. See also http://www.haskell.org/pipermail/haskell-cafe/2006-May/015609.html http://www.haskell.org/pipermail/glasgow-haskell-users/2006-May/010278.html though I don't buy the rationale there. Hugs has no such restriction. I mean, such a sin should be shame for a non-strict language... It certainly bites in this case. We could define data TLeaf data TNode s1 s2 data MapShape s k where SLeaf :: MapShape TLeaf k SNode :: !Int - k - MapShape s1 k - MapShape s2 k - MapShape (TNode s1 s2) k data MapData s a where DLeaf :: MapData TLeaf a DNode :: a - MapData s1 a - MapData s2 a - MapData (TNode s1 s2) a data InsertResult s k = forall s'. InsertResult (MapShape s' k) (forall a. MapData s' a - (a, MapData s a)) insert :: Ord k = k - MapShape s k - InsertResult s k and have the compiler check that the transformations on the shape match the transformations on the data, but first we need to turn lots of lets into cases and erase the tildes. Of course the resulting program no longer works, but it does have verifiably correct transformations. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
Hi folks [EMAIL PROTECTED] wrote: Btw, why are there no irrefutable patterns for GADTs? I mean, such a sin should be shame for a non-strict language... Just imagine data Eq a b where Refl :: Eq a a coerce :: Eq a b - a - b coerce ~Refl a = b coerce undefined True :: String Bang you're dead. Or rather... Twiddle you're dead. Moral: in a non-total language, if you're using indexing to act as evidence for something, you need to be strict about checking the evidence before you act on it, or you will be vulnerable to the blandishments of the most appalling liars. As Randy Pollack used to say to us when we were children, the best thing about working in a strongly normalizing language is not having to normalize things. All the best Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Sep 19, 2006, at 8:52 AM, Conor McBride wrote: Hi folks [EMAIL PROTECTED] wrote: Btw, why are there no irrefutable patterns for GADTs? I mean, such a sin should be shame for a non-strict language... Just imagine data Eq a b where Refl :: Eq a a coerce :: Eq a b - a - b coerce ~Refl a = b I think you mean: coerce ~Refl x = x coerce undefined True :: String Bang you're dead. Or rather... Twiddle you're dead. Moral: in a non-total language, if you're using indexing to act as evidence for something, you need to be strict about checking the evidence before you act on it, or you will be vulnerable to the blandishments of the most appalling liars. As Randy Pollack used to say to us when we were children, the best thing about working in a strongly normalizing language is not having to normalize things. All the best Conor Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
Robert Dockins wrote: On Sep 19, 2006, at 8:52 AM, Conor McBride wrote: Hi folks [EMAIL PROTECTED] wrote: Btw, why are there no irrefutable patterns for GADTs? I mean, such a sin should be shame for a non-strict language... Just imagine data Eq a b where Refl :: Eq a a coerce :: Eq a b - a - b coerce ~Refl a = b I think you mean: coerce ~Refl x = x Indeed I do. My original program was much safer! Thanks Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Sun, Sep 17, 2006 at 01:08:04PM +0200, [EMAIL PROTECTED] wrote: Ross Paterson wrote: It's interesting that these composed transformations don't seem to cost too much. That the composed transformations are indeed cheap is not necessarily disturbing. I meant the composition of the transformations of the tree (update or reverse insert) that Bertram does for each list element. They're cheap because they're bounded by the depth of the tree, and even cheaper if you're probing some other part of the tree. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Mon, Sep 18, 2006 at 12:23:11AM +0100, Ross Paterson wrote: To prove that (even for partial and infinite lists ps) splitSeq ps = [(a, seconds a ps) | a - nub ps] [...] we can establish, by induction on the input list, (1) fst (splitSeq' s ps) = [(a, seconds a ps) | a - nub ps, not (member a s)] (2) member x s = get x s (snd (splitSeq' s ps)) = seconds x ps Oops, nub ps should be nub (map fst ps) in each case. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
On Thu, Sep 14, 2006 at 07:51:59PM +0200, Bertram Felgenhauer wrote: It's a result of thinking about lazy evaluation, and especially lazy patterns (and let bindings) for some time. A wiki article that helped me a lot to understand these is http://www.haskell.org/hawiki/TyingTheKnot I'd like to point out the trustList function there which uses the idea of encoding the structure of a term and its actual values in different arguments, i.e. a blueprint. One view of your device is as separating the shape (blueprint) from the contents, e.g. one can split a finite map type data Map k a = Node !Int k a (Map k a) (Map k a) | Leaf into a pair of types data MapShape k = SNode !Int k (MapShape k) (MapShape k) | SLeaf data MapData a = DNode a (MapData a) (MapData a) | DLeaf (We don't even need DLeaf, as it's never examined.) We need functions fill :: a - MapShape k - MapData a update :: Ord k = k - (a - a) - MapShape k - MapData a - MapData a insert :: Ord k = k - MapShape k - (MapShape k, MapData a - (a, MapData a)) In a dependently typed language we could parameterize MapData with shapes to give more precise types: fill :: a - forall s :: MapShape k. MapData s a update :: Ord k = k - (a - a) - forall s :: MapShape k. MapData s a - MapData s a insert :: Ord k = k - forall s :: MapShape k. (exists s' :: MapShape k, MapData s' a - (a, MapData s a)) hinting that the function returned by insert reverses the effect of the insertion. It's not possible to code this with GADTs, because existentials are incompatible with irrefutable patterns, at least in GHC. Anyway, splitSeq then becomes splitSeq :: Ord a = [(a,b)] - [(a,[b])] splitSeq = fst . splitSeq' SLeaf splitSeq' :: Ord a = MapShape a - [(a,b)] - ([(a,[b])], MapData [b]) splitSeq' bp [] = ([], fill [] bp) splitSeq' bp ((a,b):xs) | member a bp = let (l, m) = splitSeq' bp xs in (l, update a (b:) bp m) | otherwise = let (bp', extract) = insert a bp (l, m')= splitSeq' bp' xs (bs, m)= extract m' in ((a, b:bs) : l, m) Again, no knot-tying is required. To prove that (even for partial and infinite lists ps) splitSeq ps = [(a, seconds a ps) | a - nub ps] where seconds :: Eq a = a - [(a,b)] - [b] seconds a ps = [b | (a', b) - ps, a' == a] we need another function get :: Ord k = k - MapShape k - MapData a - a and the properties member k s = get k s (fill v s) = v member k s = get k s (update k f s m) = f (get k s m) member k s /\ member x s /\ x /= k = get x s (update k f s m) = get x s m not (member k s) /\ insert k s = (s', extract) = member x s' = member x s || x == k not (member k s) /\ insert k s = (s', extract) = fst (extract m) = get k s' m not (member k s) /\ insert k s = (s', extract) /\ member x s = get x s (snd (extract m)) = get x s' m Then we can establish, by induction on the input list, (1) fst (splitSeq' s ps) = [(a, seconds a ps) | a - nub ps, not (member a s)] (2) member x s = get x s (snd (splitSeq' s ps)) = seconds x ps This is enough to sustain the induction and obtain the desired property, but it's a bit inelegant not to have an exact characterization of the second component. It seems essential to observe the map data only though get. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
ross: On Thu, Sep 14, 2006 at 07:51:59PM +0200, Bertram Felgenhauer wrote: It's a result of thinking about lazy evaluation, and especially lazy patterns (and let bindings) for some time. A wiki article that helped me a lot to understand these is http://www.haskell.org/hawiki/TyingTheKnot I'd like to point out the trustList function there which uses the idea of encoding the structure of a term and its actual values in different arguments, i.e. a blueprint. One view of your device is as separating the shape (blueprint) from the contents, e.g. one can split a finite map type data Map k a = Node !Int k a (Map k a) (Map k a) | Leaf into a pair of types data MapShape k = SNode !Int k (MapShape k) (MapShape k) | SLeaf data MapData a = DNode a (MapData a) (MapData a) | DLeaf ... Nice description. Ross, I added a wiki page for this technique. Would you like to either elaborate on the wiki, or include the text of your email to it? http://haskell.org/haskellwiki/Separating_shape_and_content Cheers, Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
Thanks Bertran for your solution. I have difficulty understanding it so I can't comment on it right now but I'll try to have a look at it. Do you know of any article that explains this technique, starting from very simple examples? /Magnus On Thu, 14 Sep 2006, Bertram Felgenhauer wrote: I wrote: [1] Balancing can be done with the information in the blueprint, and mapping back is easily done by doing the transformation on the tree in reverse. I should add that this possibility was the main reason for dealing with blueprints at all. As Ross Paterson's solution shows, it's possible to get simpler code without balancing the tree. regards, Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Optimization problem
Magnus Jonsson wrote: Thanks Bertran for your solution. I have difficulty understanding it so I can't comment on it right now but I'll try to have a look at it. Do you know of any article that explains this technique, starting from very simple examples? Not really. It's a result of thinking about lazy evaluation, and especially lazy patterns (and let bindings) for some time. A wiki article that helped me a lot to understand these is http://www.haskell.org/hawiki/TyingTheKnot I'd like to point out the trustList function there which uses the idea of encoding the structure of a term and its actual values in different arguments, i.e. a blueprint. HTH, Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
