Re: [Haskell] View patterns in GHC: Request for feedback

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
51 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Re: Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell] View patterns in GHC: Request for feedback

Heinrich Apfelmus
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Stefan O'Rear
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

signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request forfeedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell] View patterns in GHC: Request for feedback

haskell-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Conor McBride
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
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell] View patterns in GHC: Request for feedback

Heinrich Apfelmus
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Stefan O'Rear
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Dan Licata
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Conor McBride
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
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell] View patterns in GHC: Request for feedback

Jon Fairbairn
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Jonathan Cast
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?
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

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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request for feedback

Stefan O'Rear
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
Right, which is why I think the functional dependency is good.  If we
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request forfeedback

Jacques Carette
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: [Haskell] View patterns in GHC: Request?for?feedback

David Roundy-2
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
To give a somewhat more mundane example if you define a class Array

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
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell] View patterns in GHC: Request?for?feedback

Aaron Denney
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
123