On Jul25, Benjamin Franksen wrote:
> Dan Licata wrote: > > On Jul25, apfelmus wrote: > >> The point is to be > >> able to define both zip and pairs with one and the same operator :< . > > > > There's actually a quite simple way of doing this. You make the view > > type polymorphic, but not in the way you did: > > > > type Queue elt > > empty :: Queue elt > > cons :: elt -> Queue elt -> Queue elt > > > > data ViewL elt rec = EmptyL > > | elt :< rec > > > > view :: Queue elt -> ViewL elt (Queue elt) > > view2 :: Queue elt -> ViewL elt (ViewL elt (Queue elt)) > > This is cool! The more so because 'view2' can quite easily be defined in > terms of 'view' > > view2 q = case view q of > EmptyL -> EmptyL > x :< q' -> x :< view q' > > so it suffices to provide the one-level 'view' as a library function. Right. The way I usually do it is to define, e.g., viewGen :: (Queue elt -> a) -> Queue elt -> ViewL elt a -- expose one level, applying the input to the subterms And then externally you can define view :: Queue elt -> ViewL elt (Queue elt) view = viewGen id view2 :: Queue elt -> ViewL elt (ViewL elt (Queue elt)) view2 = viewGen view etc. > Does this scale to views containing multiple nestable constructors? I'm not sure quite what you mean? Multiple datatype constructors, rather than just 2? Certainly. Multiple mutually recursive types? Yes, but you need one parameter to each view type for each type in the loop. The main limitation is that you have to program in a style where you first define the deep view function that you need and then you use it. This is somewhat syntactically inconvenient if you have a lot of "view" idioms that you only use once or twice. Of course, then you can just go back to stringing out the cases. -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dan Licata
Dan Licata wrote:
> There's actually a quite simple way of doing this. You make the view > type polymorphic, but not in the way you did: > > myzip :: Queue a -> Queue b -> Queue (a,b) > myzip a b = case (view a, view b) of > (EmptyL, _) -> empty > (_, EmptyL) -> empty > (h1 :< t1, h2 :< t2) -> (h1,h2) `cons` myzip a b > > pairs :: Queue a -> Queue (a,a) > pairs a = case view2 a of > h1 :< (h2 :< t) -> (h1, h2) `cons` pairs t > _ -> empty > > The only difference with view patterns is that you can do the view2 > inside the pattern itself: > > pairs (view2 -> h1 :< (h2 :< t)) = (h1,h2) `cons` pairs t > pairs _ = empty > > This would be useful if the thing you were viewing were deep inside > another pattern. Well, the main feature of view patterns is that you can nest them. In other words, the canonical way of writing pairs would be pairs (view -> h1 :< (view -> h2 :< t)) = (h1,h2) `cons` pairs t pairs _ = empty Nesting means to decide "later" on how to pattern match the nested part. With view2, you have to make this decision before, something I want to avoid. For example, take the (silly) definition foo :: Queue a -> Queue a foo xs = case view xs of x :< (y :< zs) -> x `cons` zs x :< ys -> ys EmptyL -> empty Here, ys is a Queue and (y :< zs) is a ViewL. By scrutinizing xs via view , both have to be a Queue. By scrutinizing it via view2 , both have to be a ViewL. But I want to mix them. The idea is to introduce a new language extension, namely the ability to pattern match a polymorphic type. For demonstration, let class ViewInt a where view :: Integer -> a instance ViewInt [Bool] where view n = ... -- binary representation data Nat = Zero | Succ Nat instance ViewInt Nat where view n = ... -- representation as peano number be some views of the integers. Now, I'd like to be able to write bar :: (forall a . ViewInt a => a) -> String bar Zero = ... bar (True:xs) = ... Here, the patterns have different types but the key is that is unproblematic since the polymorphic type is capable of unifying with each one. Given this language extension, we can make foo a valid definition by using a polymorphic type as the second component of :< data ViewL = EmptyL | Integer :< (forall a . ViewInt a => a) In the end, the double-negation translation Integer => (forall a . ViewInt a => a) can even be done implicitly and for all types. Together with the magic class View, this would give real views. Jón Fairbairn wrote: > It's essential to this idea that it doesn't involve any new > pattern matching syntax; the meaning of pattern matching for > overloaded functions should be just as transparent as for > non-overloaded ones. That's what the real views would do modulo the probably minor inconvenience that one would need to use (:<) and (EmptyL) instead of (:) and []. I doubt that the latter can be reused. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Wed, Jul 25, 2007 at 09:35:32PM +0200, apfelmus wrote:
> Integer > => (forall a . ViewInt a => a) > > can even be done implicitly and for all types. Together with the magic > class View, this would give real views. > > > Jón Fairbairn wrote: > > It's essential to this idea that it doesn't involve any new > > pattern matching syntax; the meaning of pattern matching for > > overloaded functions should be just as transparent as for > > non-overloaded ones. > > That's what the real views would do modulo the probably minor > inconvenience that one would need to use (:<) and (EmptyL) instead of > (:) and []. I doubt that the latter can be reused. desugaring without altering the typechecking kernel at all. (for simplicity of exposition, assume pattern matches have already been compiled to flat cases using Johnsson's algorithm; in particular the patterns mentioned consist of exactly one constructor, not zero) case scrut of pat -> a _ -> b ==> realcase (Prelude.view scrut) of pat -> a _ -> b Where in the Prelude (or the current type environment, if -fno-implicit-prelude) we have: class View a c | c -> a where view :: a -> c and we provide a deriving-form for View which generates View Foo Foo where view = id. Or, a rule which does that automatically if no explicit instance of View _ Foo is in the current module. Or, remove the fundep and add an instance View a a where view = id to the Prelude. Option 3 makes definitions more polymorphic. Options 1 and 2 keep the same level of polymorphism as before; 1 is simpler but breaks old code. Note that none of these options supports the value input feature; we need new syntax to support non-binding identifiers in patterns! Stefan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment |
In reply to this post by Heinrich Apfelmus
On Jul25, apfelmus wrote:
> Dan Licata wrote: > > There's actually a quite simple way of doing this. You make the view > > type polymorphic, but not in the way you did: > > > > myzip :: Queue a -> Queue b -> Queue (a,b) > > myzip a b = case (view a, view b) of > > (EmptyL, _) -> empty > > (_, EmptyL) -> empty > > (h1 :< t1, h2 :< t2) -> (h1,h2) `cons` myzip a b > > > > pairs :: Queue a -> Queue (a,a) > > pairs a = case view2 a of > > h1 :< (h2 :< t) -> (h1, h2) `cons` pairs t > > _ -> empty > > > > The only difference with view patterns is that you can do the view2 > > inside the pattern itself: > > > > pairs (view2 -> h1 :< (h2 :< t)) = (h1,h2) `cons` pairs t > > pairs _ = empty > > > > This would be useful if the thing you were viewing were deep inside > > another pattern. > > Well, the main feature of view patterns is that you can nest them. In > other words, the canonical way of writing pairs would be > > pairs (view -> h1 :< (view -> h2 :< t)) = (h1,h2) `cons` pairs t > pairs _ = empty > > Nesting means to decide "later" on how to pattern match the nested part. > With view2, you have to make this decision before, something I want to > avoid. > > For example, take the (silly) definition > > foo :: Queue a -> Queue a > foo xs = case view xs of > x :< (y :< zs) -> x `cons` zs > x :< ys -> ys > EmptyL -> empty > > Here, ys is a Queue and (y :< zs) is a ViewL. By scrutinizing xs > via view , both have to be a Queue. By scrutinizing it via view2 , > both have to be a ViewL. But I want to mix them. > > The idea is to introduce a new language extension, namely the ability to > pattern match a polymorphic type. For demonstration, let > > class ViewInt a where > view :: Integer -> a > > instance ViewInt [Bool] where > view n = ... -- binary representation > > data Nat = Zero | Succ Nat > > instance ViewInt Nat where > view n = ... -- representation as peano number > > be some views of the integers. Now, I'd like to be able to write > > bar :: (forall a . ViewInt a => a) -> String > bar Zero = ... > bar (True:xs) = ... This doesn't make sense to me: Zero :: Nat and therefore Zero :: ViewInt Nat => Nat but you can't generalize from that to Zero :: forall a. ViewInt a => a E.g., Zero does not have type ViewInt [Bool] => Bool Maybe you wanted an existential instead, and what you're writing is sugar for bar :: (exists a . ViewInt a => a) -> String bar (pack[Nat](view[Nat] -> Zero)) = ... bar (pack[Bool List](view[Bool List] -> True:xs)) = ... (where I'm using [] to make the polymorphic instantiations clear). That is, you open the existential, and then use the view function at the the unpacked type in each case and match against the result. Note that matching against types like this is a form of intensional type analysis. -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
On Jul25, Claus Reinke wrote:
> although you could introduce a _convention_ by which all view functions > are supposed to be exhaustive over their input type, the types themselves > do not encode or check exhaustiveness. so we're talking about an informal > promise rather than a formal guarantee. Oh! I had assumed that it was already considered rude to expose a non-exhaustive function to the outside world: As far as I know there's no way to handle the match error (at least in pure code), such as handle Match in SML, or your lambda-match stuff on the Haskell' list. So how can a client use such a function? Either he has to do a check first (if canCallF x then f x else ...) or he has to know for other reasons that the precondition holds. In either case, it seems like the right thing to do is to encode the precondition in the type system (if only using abstract types, so the implementation of the module is still unverified). > one could turn that promise into a type-checked guarantee by using > explicit sum types (and thus structural rather than name-based typing), > but that gets awkward in plain haskell. I don't think the choice of whether you label your variants with names or with numbers (in1, in2, in3...) has anything to do with the choice of whether you require your cases to be exhaustive or not. > i often feel limited by the non-extensible, need-to-be-named sum > types in haskell, and since i intend to use view patterns to encode > abstract patterns, within a framework of extensible matching, i > encoded my patterns in an extensible, open fashion. And if you're using extensible sums, then there always is an extra case to consider, since there are always potential future extensions that you don't know about. So that's a perfect time to use the Maybes. But I still maintain that it's wrong to use the outUnit/outArrow style when what you are defining is in fact a total function into a closed sum type, since the type of outUnit/outArrow captures what is going on less precisely. (Even though neither type captures what is going on exactly, since they both admit the possibility of exceptions/non-termination.) > i just wanted to suggest that it might be possible to get the best of > both worlds: documentation of exhaustiveness and extensible matches > (see Tullsen's first-class patterns or my library support and examples > for lambda-match on the haskell-prime list for more discussion of the > latter). The way I'd support documentation of exhaustiveness would be to add a modality of "pure" (exhaustive, terminating, can't raise an exception, no unsafePerformIO, ...) code to Haskell. Then you could document the fact that a view function is really total in its type. I'm not quite sure how this modality would work, though. -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Jon Fairbairn
Jon Fairbairn wrote:
> I currently only get f :: [t] -> something, so if I later > discover that I need to change the input representation to > be more efficient than lists, I have to rewrite f. Wouldn't > it be so much nicer if I could simply add a declaration > >> f:: Stream s => s t -> something > > and get a function that works on anything in the Stream > class? > > The core of the idea would be to allow classes to include > constructors (and associated destructors) so the definition > of Stream would include something for ":" and "[]" and their > inverses, though I've no real idea of the details; can > anyone come up with a plan? I had been avoiding adding my two cents, but I must object to this. Because this is starting to sound like one of the maddening things about C++. Namely, the automatic implicit casting conversions of classes via their single argument constructors. This is one of the (several) things that makes reading and understanding a function or method call in C++ incredibly difficult. What if the 'f' in the quoted message above is itself part of a type class. Then one has to decide which instance 'f' is being called and what constructors/destructors are being called to view the 's t' parameter as the correct concrete type. That way lies madness. Any magical view logic is dangerous in this respect. Thus I would probably not want any special implicit (class View a b) or (call View a b | a -> b), etc. At least the proposal that (=> _) is (-> Just _) makes you change the syntax instead of overloading (->). -- Chris _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dan Licata
Hi Dan
On 25 Jul 2007, at 15:18, Dan Licata wrote: > Hi Conor, > [..] > Why are you so fatalistic about "with" in Haskell? I guess I'm just fatalistic, generally. Plausibility is not something I'm especially talented at. > Is it harder to > implement than it looks? For Haskell, it ought to be very easy. > It seems to be roughly in the same category as > our view pattern proposal, in that it's just an addition to the syntax > of pattern matching, and it has a straightforward elaboration into the > internal language. Even on the source level, the with-blocks just expand as "helper functions". I wonder if I have the time and energy to knock up a preprocessor... > (Well, for Haskell it's more straightforward than > for Epigram, because we don't need to construct the evidence for > ruling > out contradictory branches, etc., necessary to translate to inductive > family elims.) In the dependently typed setting, it's often the case that the "with-scrutinee" is an expression of interest precisely because it occurs in the *type* of the function being defined. Correspondingly, an Epigram implementation should (and the Agda 2 implementation now does) abstract occurrences of the expression from the type. That makes things a bit trickier to implement, but it's just the thing you need to replace "stuck" computations in types with actual values. The "with" construct is what makes it possible to keep all the layers of computation in step. It's so often exactly the thing you need in dependently typed programming, so maybe that's a point in its favour as a conceivable Haskell feature, given the flow of the type-level computation tide. All the best Conor _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dan Licata
Dan Licata wrote:
> apfelmus wrote: >> The idea is to introduce a new language extension, namely the ability to >> pattern match a polymorphic type. For demonstration, let >> >> class ViewInt a where >> view :: Integer -> a >> >> instance ViewInt [Bool] where >> view n = ... -- binary representation >> >> data Nat = Zero | Succ Nat >> >> instance ViewInt Nat where >> view n = ... -- representation as peano number >> >> be some views of the integers. Now, I'd like to be able to write >> >> bar :: (forall a . ViewInt a => a) -> String >> bar Zero = ... >> bar (True:xs) = ... > > This doesn't make sense to me: > > Zero :: Nat > > and therefore > > Zero :: ViewInt Nat => Nat > > but you can't generalize from that to > > Zero :: forall a. ViewInt a => a > > E.g., Zero does not have type ViewInt [Bool] => Bool Yes, the types of the patterns don't unify. But each one is a specialization of the argument type. Note that the type signature is bar :: (forall a . ViewInt a => a) -> String which is very different from bar :: forall a . ViewInt a => a -> String Without the extension, we would write bar as follows bar :: (forall a . ViewInt a => a) -> String bar x = let xNat = x :: Nat in case xNat of Zero -> ... _ -> let xListBool = x :: [Bool] in case xListBool of True:xs -> ... In other words, we can specialize the polymorphic argument to each pattern type and each equation may match successfully. > Maybe you wanted an existential instead No. That would indeed mean to pick the matching equation by analysing the packed type, i.e. some equations don't match since their patterns have the wrong type. I think that such a thing violates parametricity. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Conor McBride
> In the dependently typed setting, it's often the case that the
> "with-scrutinee" is an expression of interest precisely because it > occurs > in the *type* of the function being defined. Correspondingly, an > Epigram implementation should (and the Agda 2 implementation now does) > abstract occurrences of the expression from the type. That makes things > a bit trickier to implement, but it's just the thing you need to replace > "stuck" computations in types with actual values. The "with" construct > is what makes it possible to keep all the layers of computation in step. Oh, I see: you use 'with' as a heuristic for guessing the motive of the inductive family elim. How do you pick which occurrences of the with-scrutinee to refine, and which to leave as a reference to the original variable? You don't always want to refine all of them, do you? -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Stefan O'Rear
I think what you're describing is equivalent to making the "implicit
view function" syntax so terse that you don't write anything at all. So the pattern 'p' is always (view -> p). This seems like a pretty invasive change: I don't think the version with the functional dependency works (unless you adopt some form of scoped type class instances, as you suggest below), because then if you want to use a datatype as a view, you can no longer pattern match on the datatype itself at all! Even with some form of scoping, you can't decompose the view datatype as itself and as a view in the same scope. The non-functional type class will make everything very polymorphic (e.g., where we used to infer a type based on the datatype constructors that occurred, we will now say that it's anything that can be viewed as that datatype). So, this syntax affects a lot of code, existing or otherwise, that doesn't use view patterns, which is something we're trying to avoid. -Dan On Jul25, Stefan O'Rear wrote: > On Wed, Jul 25, 2007 at 09:35:32PM +0200, apfelmus wrote: > > Integer > > => (forall a . ViewInt a => a) > > > > can even be done implicitly and for all types. Together with the magic > > class View, this would give real views. > > > > > > Jón Fairbairn wrote: > > > It's essential to this idea that it doesn't involve any new > > > pattern matching syntax; the meaning of pattern matching for > > > overloaded functions should be just as transparent as for > > > non-overloaded ones. > > > > That's what the real views would do modulo the probably minor > > inconvenience that one would need to use (:<) and (EmptyL) instead of > > (:) and []. I doubt that the latter can be reused. > > It's possible to go even simpler, and implement views via a simple > desugaring without altering the typechecking kernel at all. > > (for simplicity of exposition, assume pattern matches have already been > compiled to flat cases using Johnsson's algorithm; in particular the > patterns mentioned consist of exactly one constructor, not zero) > > case scrut of > pat -> a > _ -> b > > ==> > > realcase (Prelude.view scrut) of > pat -> a > _ -> b > > Where in the Prelude (or the current type environment, if > -fno-implicit-prelude) we have: > > class View a c | c -> a where > view :: a -> c > > and we provide a deriving-form for View which generates View Foo Foo > where view = id. > > Or, a rule which does that automatically if no explicit instance of View > _ Foo is in the current module. > > Or, remove the fundep and add an instance View a a where view = id to > the Prelude. > > Option 3 makes definitions more polymorphic. Options 1 and 2 keep the > same level of polymorphism as before; 1 is simpler but breaks old code. > > Note that none of these options supports the value input feature; we > need new syntax to support non-binding identifiers in patterns! > > Stefan > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, Jul 26, 2007 at 11:28:03AM -0400, Dan Licata wrote:
> I think what you're describing is equivalent to making the "implicit > view function" syntax so terse that you don't write anything at all. So > the pattern 'p' is always (view -> p). Thanks, I wouldn't have thought of such a simple explanation myself :) > This seems like a pretty invasive change: > > I don't think the version with the functional dependency works (unless > you adopt some form of scoped type class instances, as you suggest > below), because then if you want to use a datatype as a view, you can no > longer pattern match on the datatype itself at all! Even with some form > of scoping, you can't decompose the view datatype as itself and as a > view in the same scope. Right, you can't pattern match on a type that is used as a view. But from what I've seen in library code, that usually doesn't happen - nobody matches ViewL except with viewl in the scrutinee, etc. You could create a proxy type (at some cost in ugliness) in the cases where you want to use the same structure for a concrete type and a view. > The non-functional type class will make everything very polymorphic > (e.g., where we used to infer a type based on the datatype constructors > that occurred, we will now say that it's anything that can be viewed as > that datatype). That's exactly the typing problem that I ... no wait I didn't actually mention it. :) > So, this syntax affects a lot of code, existing or otherwise, that > doesn't use view patterns, which is something we're trying to avoid. Eh? I *think* the typing rules are the same for the no-view case. If the auto-deriving hack isn't implemented, you only need a deriving(View), otherwise there should be no change at all... Stefan > > It's possible to go even simpler, and implement views via a simple > > desugaring without altering the typechecking kernel at all. > > > > (for simplicity of exposition, assume pattern matches have already been > > compiled to flat cases using Johnsson's algorithm; in particular the > > patterns mentioned consist of exactly one constructor, not zero) > > > > case scrut of > > pat -> a > > _ -> b > > > > ==> > > > > realcase (Prelude.view scrut) of > > pat -> a > > _ -> b > > > > Where in the Prelude (or the current type environment, if > > -fno-implicit-prelude) we have: > > > > class View a c | c -> a where > > view :: a -> c > > > > and we provide a deriving-form for View which generates View Foo Foo > > where view = id. > > > > Or, a rule which does that automatically if no explicit instance of View > > _ Foo is in the current module. > > > > Or, remove the fundep and add an instance View a a where view = id to > > the Prelude. > > > > Option 3 makes definitions more polymorphic. Options 1 and 2 keep the > > same level of polymorphism as before; 1 is simpler but breaks old code. > > > > Note that none of these options supports the value input feature; we > > need new syntax to support non-binding identifiers in patterns! > > > > Stefan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment |
On Jul26, Stefan O'Rear wrote:
> > So, this syntax affects a lot of code, existing or otherwise, that > > doesn't use view patterns, which is something we're trying to avoid. > > Eh? I *think* the typing rules are the same for the no-view case. If > the auto-deriving hack isn't implemented, you only need a > deriving(View), otherwise there should be no change at all... Assuming you don't have the functional dependency: "affects" in the sense that any code you write has a generalized type, so you have to explain view patterns to beginners right out of the gate, etc. If you write length [] = [] length (h : t) = 1 + length t we don't want to have to explain to beginners why it has type length :: forall a,b,c. View a [b] -> a -> Num c -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Heinrich Apfelmus
On Jul26, apfelmus wrote:
> Yes, the types of the patterns don't unify. But each one is a > specialization of the argument type. Note that the type signature is > > bar :: (forall a . ViewInt a => a) -> String > > which is very different from > > bar :: forall a . ViewInt a => a -> String > > Without the extension, we would write bar as follows > > bar :: (forall a . ViewInt a => a) -> String > bar x = let xNat = x :: Nat in > case xNat of > Zero -> ... > _ -> let xListBool = x :: [Bool] in > case xListBool of > True:xs -> ... > > In other words, we can specialize the polymorphic argument to each > pattern type and each equation may match successfully. Oh, I understand what you're saying now. Thanks for clarifying! -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Jon Fairbairn
Me:
> > In the dependently typed setting, it's often the case that the > > "with-scrutinee" is an expression of interest precisely because it > > occurs > > in the *type* of the function being defined. Correspondingly, an > > Epigram implementation should (and the Agda 2 implementation now does) > > abstract occurrences of the expression from the type. Dan: > Oh, I see: you use 'with' as a heuristic for guessing the motive of the > inductive family elim. How do you pick which occurrences of the > with-scrutinee to refine, and which to leave as a reference to the > original variable? You don't always want to refine all of them, do you? There are two components to this process, and they're quite separable. Let's have an example (in fantasy dependent Haskell), for safe lookup. defined :: Key -> [(Key, Val)] -> Bool defined k [] = False defined k ((k', _) : kvs) = k == k' || defined k kvs data Check :: Bool -> * where OK :: Check True lookup :: (k :: Key; kvs :: [(Key, Val)]) -> Check (defined k kvs) -> Val lookup k [] !! -- !! refutes Check False; no rhs {-before-} lookup k ((k', v) : kvs) p with k == k' {-after-} lookup k ((k', v) : kvs) OK | True = v lookup k ((k', v) : kvs) p' | False = lookup k kvs p' Left-hand sides must refine a 'problem', initially lookup k kvs p where k :: Key; kvs :: [(Key, Value)]; p :: Check (defined k kvs) Now, {-before-} the with, we have patterns refining the problem lookup k ((k', v) : kvs) p where k, k' :: Key v :: Val kvs :: [(Key, Val)] p :: Check (k == k' || defined k kvs) The job of "with" is only to generate the problem which the lines in its block must refine. We introduce a new variable, abstracting all occurrences of the scrutinee. In this case, we get the new problem {-after-}. lookup k ((k', v) : kvs) p | b where k, k' :: Key v :: Val kvs :: [(Key, Val)] b :: Bool p :: Check (b || defined k kvs) All that's happened is the abstraction of (k == k'): no matching, no mucking about with eliminators and motives. Now, when it comes to checking the following lines, we're doing the same job to check dependent patterns (translating to dependent case analysis, with whatever machinery is necessary) refining the new problem. Now, once b is matched with True or False, the type of p computes to something useful. So there's no real guesswork here. Yes, it's true that the choice to abstract all occurrences of the scrutinee is arbitrary, but "all or nothing" are the only options which make sense without a more explicit mechanism to pick the occurrences you want. Such a mechanism is readily conceivable: at worst, you just introduce a helper function with an argument for the value of the scrutinee and write its type explicitly. I guess it's a bit weird having more structure to the left-hand side. The approach here is to allow the shifting of the problem, rather than to extend the language of patterns. It's a much better fit to our needs. Would it also suit Haskell? Cheers Conor _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by haskell-2
ChrisK <[hidden email]> writes:
> Jon Fairbairn wrote: > > I currently only get f :: [t] -> something, so if I later > > discover that I need to change the input representation to > > be more efficient than lists, I have to rewrite f. Wouldn't > > it be so much nicer if I could simply add a declaration > > > >> f:: Stream s => s t -> something > > and get a function that works on anything in the Stream > > class? > > The core of the idea would be to allow classes to include > > constructors (and associated destructors) so the definition > > of Stream would include something for ":" and "[]" and their > > inverses, though I've no real idea of the details; can > > anyone come up with a plan? > > I had been avoiding adding my two cents, but I must object to this. > > Because this is starting to sound like one of the > maddening things about C++. > > Namely, the automatic implicit casting conversions of > classes via their single argument constructors. Unfortunately I'm not sufficiently familiar with C++ to know what this means. Perhaps you could clarify? Despite the obvious interpretation of my message (ahem), I'm not advocating much that's automatic. In the case of lists I was imagining that they would be the default for Streams in much the same way that Integer is the default for Num. I'd be happy to discard that part of the idea (though I'd expect howls of protest from those who want lists to be ruling class citizens). > What if the 'f' in the quoted message above is itself part > of a type class. Then one has to decide which instance 'f' > is being called and what constructors/destructors are being > called to view the 's t' parameter as the correct concrete > type. That way lies madness. Again, I think the difficulty here is a discrepancy between the interpretation of what I wrote and what I intended to mean :-), viz that classes could (in addition to their usual functions) define constructor/deconstructor pairs that would be used in desugaring pattern matching. I didn't mean that constructors of the same name could appear both in classes and in data declarations. So if one had something like class Stream s where Cons:: a -> s a -> s a Nil:: s a Snoc:: s a -> a -> s a ... {- an instance definition for Stream would have to somehow give both construction and deconstruction functions for Cons and Nil -} then a definition of the form f Nil = ... f (Cons h t) = ... would be unambiguously f:: Stream s => s a -> ... (in the absence of defaulting). There are issues about checking coverage of cases, but I don't think that's the problem you were raising? -- Jón Fairbairn [hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Friday 27 July 2007, Jon Fairbairn wrote:
> ChrisK <[hidden email]> writes: > > Jon Fairbairn wrote: > > > I currently only get f :: [t] -> something, so if I later > > > discover that I need to change the input representation to > > > be more efficient than lists, I have to rewrite f. Wouldn't > > > it be so much nicer if I could simply add a declaration > > > > > >> f:: Stream s => s t -> something > > > > > > and get a function that works on anything in the Stream > > > class? > > > The core of the idea would be to allow classes to include > > > constructors (and associated destructors) so the definition > > > of Stream would include something for ":" and "[]" and their > > > inverses, though I've no real idea of the details; can > > > anyone come up with a plan? > > > > I had been avoiding adding my two cents, but I must object to this. > > > > Because this is starting to sound like one of the > > maddening things about C++. > > > > Namely, the automatic implicit casting conversions of > > classes via their single argument constructors. > > Unfortunately I'm not sufficiently familiar with C++ to know > what this means. Perhaps you could clarify? freely, and in Classic C, you could mix pointers and integers freely, and thought this was /such/ a wonderful idea that C++ has special syntax to declare the conversion functions allowing you to, say, mix pointers and pointer-like classes freely, or to mix char*s and strings freely, etc. It's what makes template<alpha> class AutoPtr<alpha>{ alpha *ptr; public: explicit AutoPtr(){ ptr = new alpha; } AutoPtr(alpha *p){ ptr = p; } ~AutoPtr(){ delete ptr; } alpha &operator *(){ return *ptr; } operator (alpha*)(){ return ptr; }}; template<alpha> external void swap(alpha *, alpha *); ... AutoPtr<int> ptr1; AutoPtr<int> ptr2; ... swap (ptr1, ptr2); Type-check. > Despite the obvious interpretation of my message (ahem), I'm > not advocating much that's automatic. In the case of lists I > was imagining that they would be the default for Streams in > much the same way that Integer is the default for Num. I'd > be happy to discard that part of the idea (though I'd expect > howls of protest from those who want lists to be ruling > class citizens). > > > What if the 'f' in the quoted message above is itself part > > of a type class. Then one has to decide which instance 'f' > > is being called and what constructors/destructors are being > > called to view the 's t' parameter as the correct concrete > > type. That way lies madness. > > Again, I think the difficulty here is a discrepancy between > the interpretation of what I wrote and what I intended to > mean :-), viz that classes could (in addition to their usual > functions) define constructor/deconstructor pairs that would > be used in desugaring pattern matching. I didn't mean that > constructors of the same name could appear both in classes > and in data declarations. So if one had something like > > class Stream s where > Cons:: a -> s a -> s a > Nil:: s a > Snoc:: s a -> a -> s a > ... > > {- an instance definition for Stream would have to > somehow give both construction and deconstruction > functions for Cons and Nil -} > > then a definition of the form > > f Nil = ... > f (Cons h t) = ... > > would be unambiguously f:: Stream s => s a -> ... (in the > absence of defaulting). There are issues about checking > coverage of cases, but I don't think that's the problem you > were raising? -- Jonathan Cast http://sourceforge.net/projects/fid-core http://sourceforge.net/projects/fid-emacs _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe attachment0 (196 bytes) Download Attachment |
In reply to this post by Dan Licata
On Fri, Jul 27, 2007 at 05:22:37AM -0400, Dan Licata wrote:
> On Jul26, Stefan O'Rear wrote: > > > So, this syntax affects a lot of code, existing or otherwise, that > > > doesn't use view patterns, which is something we're trying to avoid. > > > > Eh? I *think* the typing rules are the same for the no-view case. If > > the auto-deriving hack isn't implemented, you only need a > > deriving(View), otherwise there should be no change at all... > > Assuming you don't have the functional dependency: "affects" in the > sense that any code you write has a generalized type, so you have to > explain view patterns to beginners right out of the gate, etc. If you > write > > length [] = [] > length (h : t) = 1 + length t > > we don't want to have to explain to beginners why it has type > > length :: forall a,b,c. View a [b] -> a -> Num c have it, and the auto-deriving hack, what breaks? length [] = [] length (h : t) = 1 + length t length :: forall a b c. (View a [b], Num c) => a -> c ==> (one of the FD rules) length :: forall a b c. (View [a] [b], Num c) => [a] -> c ==> (plain context reduction, the first constraint is tautological) length :: forall a c. Num c => [a] -> c Stefan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment |
In reply to this post by Dan Licata
Others have already pointed this out, but it is worth saying again:
Maybe is not the only monadic effect which makes sense during pattern-matching. Wolfram Kahl and I have explored some of these things as part of the Pattern Matching Calculus, http://sqrl.mcmaster.ca/~kahl/PMC/ [If you want to jump to the most recent, most complete version, see http://www.cas.mcmaster.ca/~kahl/Publications/TR/Kahl-Carette-Ji-2006b/] Various other monads can be used for pattern-matching-effects. While Maybe is quite classical, List and LogicT give extremely useful alternatives. Jacques _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Jonathan Cast
On Fri, Jul 27, 2007 at 09:02:42AM -0500, Jonathan Cast wrote:
> On Friday 27 July 2007, Jon Fairbairn wrote: > > ChrisK <[hidden email]> writes: > > > Because this is starting to sound like one of the > > > maddening things about C++. > > > > > > Namely, the automatic implicit casting conversions of > > > classes via their single argument constructors. > > > > Unfortunately I'm not sufficiently familiar with C++ to know > > what this means. Perhaps you could clarify? > > Somebody noticed that, in C, you could mix integers and floats (almost) > freely, and in Classic C, you could mix pointers and integers freely, and > thought this was /such/ a wonderful idea that C++ has special syntax to > declare the conversion functions allowing you to, say, mix pointers and > pointer-like classes freely, or to mix char*s and strings freely, etc. It's > what makes class Array { public: Array(int); // ... construct a new array of specified length ... } Then if you make the mistake of passing an integer constant to a function that expects an Array, C++ will happily construct a new Array of that size and pass that to the function. Even more exciting when you use overloading: if you define multiplication between two Arrays, then if you accidentally try to multiply an Array by an integer constant (thinking it'll be a scalar multiply), then a new Array of that size will be constructed and multiplied--almost certainly resulting in a runtime error (mismatched Array sizes), but certainly not what you want. The solution is to add explicit to the constructor for all single-argument constructors (except perhaps occasionally when you actually want explicit construction of objects). The reasoning behind this, of course, is to allow nice interactions of home-made classes such as complex numbers, or string classes (which you might want to be automatically constructed from string constants). -- David Roundy Department of Physics Oregon State University _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment |
On 2007-07-27, David Roundy <[hidden email]> wrote:
> The solution is to add explicit to the constructor for all single-argument > constructors (except perhaps occasionally when you actually want explicit > construction of objects). > > The reasoning behind this, of course, is to allow nice interactions of > home-made classes such as complex numbers, or string classes (which you > might want to be automatically constructed from string constants). I'd have thought that adding an "implicit" keyword would make more sense, and only do conversions then. But I forget, C++. -- Aaron Denney -><- _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |