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

[Simon Marlow]

Simon PJ and I are implementing view patterns, a way of pattern matching
http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns
If you have any comments or suggestions about this design, we'd love to
hear them. You can respond to this list (and we can take it to
haskell-cafe if the thread gets long) or, if you prefer, directly to me.

At the risk of being a spoil-sport, I have a somewhat negative take on view
patterns. Not because I think they're particularly bad, but because I
don't think they're significantly useful enough to warrant adding to the
language, at least if we also have pattern guards.

All of the examples on the wiki page can be written in the same number of
lines, sometimes with fewer characters, using pattern guards or some other
existing Haskell idiom (e.g. the bit parsing example is much more nicely
expressed using a bit-parsing monad). I believe adding yet another idiom
will be detrimental: too much choice is bad.

To my eyes, mixing bound and binding occurrences of variables in patterns
in an arbitrarily nested way is sure to lead to confusion. The existing
idioms all have a one-level deep notion of bound/binding scope, and in
order to get more nesting you have to start naming things: this is good,
IMO. Not that I think we should omit a language feature because it *could*
be used to write obfuscated code; no, in this case I think nesting more
than one level deep will *always* lead to obfuscated code.

The use of the right-arrow is confusing, especially on the left of a case
alternative or in a lambda expression.

it's possible that people would start routinely hiding the data
representation and exporting view functions instead, which would be an
excellent thing.

My impression is that most of the time a data structure has a clever
internal representation that you don't want to expose anyway. This is
supported by the data structures we have in the base package, all these are
abstract:

Data.Set, Data.IntSet, Data.Map, Data.IntMap
Data.Graph, Data.Sequence, Data.Bytestring, Data.Array,
Data.HashTable, Data.Ratio(Rational)

and most export view-like things (e.g. Data.Set.toList).

The modules I found that export non-abstract types that should really be
abstract:

Data.Complex, Data.Tree

So I don't think there's an overwhelming amount of stuff that would change
if we had view patterns. In GHC itself most of our data structures are
already abstract too.

The View class is nice, even with just pattern guards. I'd be in favour of
making it standard and actively encouraging its use.

Cheers,
Simon

[Jon Harrop]

Post by Simon Marlow

Simon PJ and I are implementing view patterns, a way of pattern matching
http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns
If you have any comments or suggestions about this design, we'd love to
hear them. You can respond to this list (and we can take it to
haskell-cafe if the thread gets long) or, if you prefer, directly to me.

At the risk of being a spoil-sport, I have a somewhat negative take on view
patterns...

F# already has active patterns and there are OCaml macros implementing views.
I have used F#'s active patterns extensively and find them to be extremely
useful. I can only assume that they will remain similarly useful in Haskell.

[apfelmus]

Post by Simon Marlow

Simon PJ and I are implementing view patterns, a way of pattern matching
http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns
If you have any comments or suggestions about this design, we'd love to
hear them. You can respond to this list (and we can take it to
haskell-cafe if the thread gets long) or, if you prefer, directly to me.

At the risk of being a spoil-sport, I have a somewhat negative take on
view patterns. Not because I think they're particularly bad, but
because I don't think they're significantly useful enough to warrant
adding to the language, at least if we also have pattern guards.
All of the examples on the wiki page can be written in the same number
of lines, sometimes with fewer characters, using pattern guards or some
other existing Haskell idiom (e.g. the bit parsing example is much more
nicely expressed using a bit-parsing monad). I believe adding yet
another idiom will be detrimental: too much choice is bad.

I agree that only few examples from the wiki page are that compelling.
Nevertheless, I like view patterns since they can be put to really good use

http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns#UsesofViews

Views are especially useful for Data.Graph. Also, I favor views instead
of pattern guards.

However, I don't like the current proposal, mainly because it doesn't
have the "Transparent ordinary Patterns"-feature. Also, I consider
definitions like

foldr f z [] = z
foldr f z (x : foldr f z -> xs) = x `f` xs

abuse.

Post by Simon Marlow
Data.Set, Data.IntSet, Data.Map, Data.IntMap
Data.Graph, Data.Sequence, Data.Bytestring, Data.Array,
Data.HashTable, Data.Ratio(Rational)
So I don't think there's an overwhelming amount of stuff that would
change if we had view patterns. In GHC itself most of our data
structures are already abstract too.

While the implementation of the abstract data structures themselves is
unlikely to change, views make it much easier to use them. I think it
would be a big win to have ByteStrings or Data.Sequence pattern matched
like ordinary lists and I think that Data.Graph will blossom with proper
view patterns.

Regards,
apfelmus

[Rene de Visser]

Simon PJ and I are implementing view patterns, a way of pattern matching
http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns
If you have any comments or suggestions about this design, we'd love to
hear them. You can respond to this list (and we can take it to
haskell-cafe if the thread gets long) or, if you prefer, directly to me.

I find the => operator excessive. GHC Haskell seems to be growing too
rapidly syntax wise in my opinion.
The important features of code are correctness, maintainability and
readibility (IMHO), and I think => is working against these.

=> uses up more syntax. Buys very little. Equivalent to "-> Just _ " or "->
Just x " as far as I can see.
I would prefer to type the extra 6 characters rather than having the hidden
Maybe.
It is also one more thing to learn. One more confusing type error when you
mix them up.

Rene.

[Jonathan Cast]

Post by Rene de Visser

Simon PJ and I are implementing view patterns, a way of pattern matching
http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns
If you have any comments or suggestions about this design, we'd love to
hear them. You can respond to this list (and we can take it to
haskell-cafe if the thread gets long) or, if you prefer, directly to me.

I find the => operator excessive.

I want to voice my complete agreement. At least -> is already a binding
operator in GHC, with semantics analogous to those being introduced; since
when is => a binding operator? Thus far, neither => nor <= has been used for
anything of the sort, so it's an entirely new entry in the semantic space ---
and => /is/ already a keyword in GHC, which makes it worse.

<snip>

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs

[Claus Reinke]

unit :: Typ -> Maybe ()
arrow :: Type -> Maybe (Typ,Typ)
size :: Typ -> Integer
size (unit -> ()) = 1
size (arrow -> (t1,t2)) = size t1 + size t2

size (unit -> Just ()) = 1
size (arrow -> Just (t1,t2)) = size t1 + size t2
?

actually, i might!-) it is not just that, in general, you have to invent
and declare those intermediate view types, but that their use obscures
the overall pattern, once you start nesting abstract and concrete
patterns (and if you don't nest them, view patterns don't add much).

claus

[Simon Peyton-Jones]

| At the risk of being a spoil-sport, I have a somewhat negative take on
| view patterns. Not because I think they're particularly bad, but
| because I don't think they're significantly useful enough to warrant
| adding to the language, at least if we also have pattern guards.

Syntactic sugar is always like this. It's always a judgement call: is the extra expressiveness worth the extra cost? One could ask that about list comprehensions, or pattern guards, or as-patterns, or records. Yet syntactic sugar can sometimes have quite a powerful effect -- think of do-notation for example.

The other question is about cost. Syntactic sugar that can be readily explained, is easy to implement, and involves only localized changes (to the spec and to the compiler) are cheap. The views that Dan and I propose are specifically crafted to be minimally invasive and cheap in this sense.

I swing to and fro on this one. On one day I think that view patterns are OK but just not quite worth it. On the next I think that perhaps they'll lower the barrier to allowing us to combine *abstraction* and *pattern matching*. The answer probably differs from one person to another. At the moment we're faced with this tension; pattern guards (also arguably superfluous) make it a bit easier but not easy enough.

Views have been the subject of rather inconclusive debate for a long time, certainly since the inception of Haskell. I'm thinking of pattern views as a way to break the logjam by implementing something that is a reasonable stab, and seeing whether it "sticks". I thought of pattern guards in the same way, and they certainly seem to have stuck. But we can only find out by trying it out.

That said, I'm keen to do it as well as possible -- so the more comments the better.

Simon

[apfelmus]

Post by Simon Peyton-Jones
Views have been the subject of rather inconclusive debate for a long time,
certainly since the inception of Haskell. I'm thinking of pattern

views as a way

Post by Simon Peyton-Jones
to break the logjam by implementing something that is a reasonable stab,
and seeing whether it "sticks". I thought of pattern guards in the

same way,

Post by Simon Peyton-Jones
and they certainly seem to have stuck. But we can only find out by

trying it out.

What I fear the most is exactly that this proposal "sticks" and becomes
the de-facto standard :(

IMHO, the long-time debate about views is not whether they're useful (I
think they are!) but which concrete form to choose. Unfortunately, all
of the proposals so far are somehow like Dr. Jekyll and Mr. Hyde: one
side is nice but the other is rather ugly.

In the end, I might end up using the currently proposed pattern views,
not because I'm fond of the proposal but simply because they're
implemented and the pain of not using views is too big.

Regards,
apfelmus

[Jules Bean]

Post by apfelmus
IMHO, the long-time debate about views is not whether they're useful (I
think they are!) but which concrete form to choose. Unfortunately, all
of the proposals so far are somehow like Dr. Jekyll and Mr. Hyde: one
side is nice but the other is rather ugly.
In the end, I might end up using the currently proposed pattern views,
not because I'm fond of the proposal but simply because they're
implemented and the pain of not using views is too big.

Maybe it would be helpful if Simon M would give a bit more flesh to the
bones of his suggestion that all the examples in the proposal can be
done more concisely without them.

apfelmus: Have you tried using pattern guards for views?

f s | y <: ys <- viewl s = ....
| EmptyL <- viewl s = ....

(did I get that right? :)

Personally I thought the basic proposal is quite nice, but the extra
sugar for Maybes and tuples looked a bit ugly...

Jules

[apfelmus]

Post by Jules Bean
Have you tried using pattern guards for views?
f s | y :< ys <- viewl s = ....
| EmptyL <- viewl s = ....

Hm, I'd simply use a plain old case-expression here

f s = case viewl s of
y :< ys -> ...
EmptyL -> ...

In other words, case-expressions are as powerful as any view pattern may
be in the single-parameter + no-nesting case.


A better example is probably zip for sequences (Data.Sequence.Seq):

zip :: Seq a -> Seq b -> Seq (a,b)
zip xs ys = case viewl xs of
x :< xt -> case viewl ys of
y :< yt -> (x,y) <| zip xt yt
EmptyL -> empty
EmptyL -> empty

Pattern guards

zip xs ys
| EmptyL <- viewl xs = empty
| EmptyL <- viewl ys = empty
| x :< xt <- viewl xs, y :< yt <- viewl ys = (x,y) <| zip xt yt

Pattern guards variant

zip xs ys
| EmptyL <- xs' = empty
| EmptyL <- ys' = empty
| x :< xt <- xs', y :< yt <- ys' = (x,y) <| zip xt yt
where
xs' = viewl xs; ys' = viewl ys

View patterns

zip (viewl -> EmptyL) _ = empty
zip _ (viewl -> EmptyL) = empty
zip (viewl -> x :< xs) (viewl -> y :< ys) = (x,y) <| zip xs ys

My dream

zip EmptyL _ = empty
zip _ EmptyL = empty
zip (x:<xs) (y:<ys) = (x,y) <| zip xs ys


Regards,
apfelmus

[Conor McBride]

Hi

Ok, I'm not quite under my rock yet,,,

Post by apfelmus

Post by Jules Bean
Have you tried using pattern guards for views?
f s | y :< ys <- viewl s = ....
| EmptyL <- viewl s = ....

This is annoying because the intermediate computation gets repeated. I
don't think view patterns fix this even if they sometimes hide it. I
worry
that the good behaviour of this feature depends on a compiler
noticing that
a repetition can be shared: this design makes the sharing harder to
express.

Of course,

Post by apfelmus
Hm, I'd simply use a plain old case-expression here
f s = case viewl s of
y :< ys -> ...
EmptyL -> ...

which is fine if you're ready to commit to the right-hand side at
this point,
but what if the result of the intermediate computation tells you what
patterns to look for next?

Epigram's "with"-notation was never implemented in Epigram, but it
has been
implemented in Agda 2. At the moment, we'd write

f s with viewl s -- adds a new column to the left
f s | y :< ys = ... -- so you can now match whatever you like
f s | EmptyL = ...

Inside a "with-block", the patterns left of | must refine the original
patterns left of the "with". When you're fed up looking at the new
information, you can exit the block, drop the column and carry on as
normal
(see zip, below).

I'd hope that we might ultimately be able to elide the repeated lefts
if they are unchanged, but that's not implemented at the moment.

f s with viewl s -- adds a new column to the left
| y :< ys = ...
| EmptyL = ...

So zip might become

zip xs ys with viewl xs
| x :< xt with viewl ys
| y :< yt = (x, y) <| zip xt yt
zip _ _ = empty

or even

zip xs ys with viewl xs with viewl ys
| x :< xt | y :< yt = (x, y) <| zip xt yt
zip _ _ = empty

For more entertainment, a padding zip

pzip x' xs y' ys with viewl xs with viewl ys
| x :< xt | y :< yt = (x, y) <| pzip x
xt y yt
| x :< xt | EmptyL = fmap (flip (,) y') xs
| EmptyL | y :< yt = fmap ((,) x') ys
pzip _ _ _ _ = empty

Pattern matching is much weirder in a dependently typed setting, but
also a
lot more powerful. Inspecting the value of a pattern variable or of an
intermediate computation can leave us knowing more about (and hence
instantiate) other pattern variables. We get stuff like this

gcd :: Positive -> Positive -> Positive
gcd x y with trichotomy x y
gcd x (x + y) | LT x y = gcd x y
gcd x x | EQ x = x
gcd (y + x) y | GT x y = gcd x y

Here, matching on the result of trichotomy (with constructor
patterns, see?)
causes the original argument patterns to become more informative
(with non-linear non-constructor forms which are *guaranteed* to match
at no run time cost).

For us, it's a bad idea to try to think of analysing one scrutinee
independently of the other data we have to hand. We're naturally pushed
towards thinking about the left-hand side as a whole, to which
information
can be added, supporting further refinement. This is part of what James
McKinna and I were on about in "The view from the left", and it's
happening
on real computers now.

To sum up, one-shot matching on intermediate computations, as provided
by pattern guards or view-patterns, is conspicuously nasty in a
dependently
typed language, but for reasons which make it sometimes merely
annoying in
Haskell.

I'm disinclined to argue thus: "don't do your thing (which probably will
happen) because it messes up my thing (which probably won't, at least in
Haskell)". I'll just chuck these observations in the air and see what
happens.

All the best

Conor

PS Please may I have pattern synonyms anyway? They're cheap and they
serve a
different purpose. Maybe I should say more about how their absence is
seriously nasty for the way I work, another time.

[Dan Licata]

Hi Conor,

This is a really good point, especially in the presence of GADTs and
type-level functions and so on, which introduce aspects of dependency.

Why are you so fatalistic about "with" in Haskell? Is it harder to
implement than it looks? 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. (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.)

-Dan

Post by Conor McBride
Hi
Ok, I'm not quite under my rock yet,,,

Post by apfelmus

Post by Jules Bean
Have you tried using pattern guards for views?
f s | y :< ys <- viewl s = ....
| EmptyL <- viewl s = ....

This is annoying because the intermediate computation gets repeated. I
don't think view patterns fix this even if they sometimes hide it. I
worry
that the good behaviour of this feature depends on a compiler
noticing that
a repetition can be shared: this design makes the sharing harder to
express.
Of course,

Post by apfelmus
Hm, I'd simply use a plain old case-expression here
f s = case viewl s of
y :< ys -> ...
EmptyL -> ...

which is fine if you're ready to commit to the right-hand side at
this point,
but what if the result of the intermediate computation tells you what
patterns to look for next?
Epigram's "with"-notation was never implemented in Epigram, but it
has been
implemented in Agda 2. At the moment, we'd write
f s with viewl s -- adds a new column to the left
f s | y :< ys = ... -- so you can now match whatever you like
f s | EmptyL = ...
Inside a "with-block", the patterns left of | must refine the original
patterns left of the "with". When you're fed up looking at the new
information, you can exit the block, drop the column and carry on as
normal
(see zip, below).
I'd hope that we might ultimately be able to elide the repeated lefts
if they are unchanged, but that's not implemented at the moment.
f s with viewl s -- adds a new column to the left
| y :< ys = ...
| EmptyL = ...
So zip might become
zip xs ys with viewl xs
| x :< xt with viewl ys
| y :< yt = (x, y) <| zip xt yt
zip _ _ = empty
or even
zip xs ys with viewl xs with viewl ys
| x :< xt | y :< yt = (x, y) <| zip xt yt
zip _ _ = empty
For more entertainment, a padding zip
pzip x' xs y' ys with viewl xs with viewl ys
| x :< xt | y :< yt = (x, y) <| pzip x
xt y yt
| x :< xt | EmptyL = fmap (flip (,) y') xs
| EmptyL | y :< yt = fmap ((,) x') ys
pzip _ _ _ _ = empty
Pattern matching is much weirder in a dependently typed setting, but
also a
lot more powerful. Inspecting the value of a pattern variable or of an
intermediate computation can leave us knowing more about (and hence
instantiate) other pattern variables. We get stuff like this
gcd :: Positive -> Positive -> Positive
gcd x y with trichotomy x y
gcd x (x + y) | LT x y = gcd x y
gcd x x | EQ x = x
gcd (y + x) y | GT x y = gcd x y
Here, matching on the result of trichotomy (with constructor
patterns, see?)
causes the original argument patterns to become more informative
(with non-linear non-constructor forms which are *guaranteed* to match
at no run time cost).
For us, it's a bad idea to try to think of analysing one scrutinee
independently of the other data we have to hand. We're naturally pushed
towards thinking about the left-hand side as a whole, to which
information
can be added, supporting further refinement. This is part of what James
McKinna and I were on about in "The view from the left", and it's
happening
on real computers now.
To sum up, one-shot matching on intermediate computations, as provided
by pattern guards or view-patterns, is conspicuously nasty in a
dependently
typed language, but for reasons which make it sometimes merely
annoying in
Haskell.
I'm disinclined to argue thus: "don't do your thing (which probably will
happen) because it messes up my thing (which probably won't, at least in
Haskell)". I'll just chuck these observations in the air and see what
happens.
All the best
Conor
PS Please may I have pattern synonyms anyway? They're cheap and they
serve a
different purpose. Maybe I should say more about how their absence is
seriously nasty for the way I work, another time.
_______________________________________________
Haskell-Cafe mailing list
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Conor McBride]

Hi Dan

Post by Dan Licata
Hi Conor,

[..]

Post by Dan Licata
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.

Post by Dan Licata
Is it harder to
implement than it looks?

For Haskell, it ought to be very easy.

Post by Dan Licata
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...

Post by Dan Licata
(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

[Dan Licata]

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

[Benjamin Franksen]

Post by apfelmus

Post by Jules Bean
Have you tried using pattern guards for views?
f s | y :< ys <- viewl s = ....
| EmptyL <- viewl s = ....

Hm, I'd simply use a plain old case-expression here
f s = case viewl s of
y :< ys -> ...
EmptyL -> ...
In other words, case-expressions are as powerful as any view pattern may
be in the single-parameter + no-nesting case.
zip :: Seq a -> Seq b -> Seq (a,b)
zip xs ys = case viewl xs of
x :< xt -> case viewl ys of
y :< yt -> (x,y) <| zip xt yt
EmptyL -> empty
EmptyL -> empty

This is how I do it, no pattern guards, no view patterns:

zip :: Seq a -> Seq b -> Seq (a,b)
zip xs ys = case (viewl xs,viewl ys) of
(EmptyL, _ ) -> empty
(_, EmptyL ) -> empty
(x :< xt, y :< yt) -> (x,y) <| zip xt yt

This is IMHO a lot clearer than any of the alternatives you listed, except
your 'dream' (which is exactly what 'real' views would give us).

Cheers
Ben, member of the we-want-real-views-or-nothing-at-all movement ;-)

[apfelmus]

Post by apfelmus

Post by apfelmus
In other words, case-expressions are as powerful as any view pattern may
be in the single-parameter + no-nesting case.

zip :: Seq a -> Seq b -> Seq (a,b)
zip xs ys = case (viewl xs,viewl ys) of
(EmptyL, _ ) -> empty
(_, EmptyL ) -> empty
(x :< xt, y :< yt) -> (x,y) <| zip xt yt
This is IMHO a lot clearer than any of the alternatives you listed, except
your 'dream' (which is exactly what 'real' views would give us).

Splendid! That lifts the single-parameter restriction. Let's also lift
the no-nesting restriction with an audacious use of rank-2-polymorphism!
The idea is that we may match a polymorphic type (forall a . a) against
as many different pattern types as we wish. In other words, the definition

foo :: (forall a . a) -> String
foo x = case x of
"eek" -> ...
13 -> ...
(x,y) -> ...

should be just fine. Of course we need a class context like (forall a .
View b a => a) for a polymorphic type to be useful.

Here's (almost) a demonstration for sequence types, the code works with
hugs -98.

class View a b | b -> a where
view :: a -> b

data Queue a = ...

instance View (Queue a) (Queue a) where
view = id

The view from the left is

data ViewL seq a = EmptyL | a :< (forall b . View (seq a) b => b)

where the key trick is to make the second component of :< polymorphic.

instance View (Queue a) (ViewL Queue a) where
view q = if null q then EmptyL else head q :< view (tail q)

The zip function can be defined just like before

zip :: Queue a -> Queue b -> Queue (a,b)
zip xs ys = case (view xs, view ys) of
(EmptyL, _ ) -> empty
(_, EmptyL ) -> empty
(x :< xt, y :< yt) -> (x,y) `cons` zip xt yt

But now, we can even nest patterns

pairs :: Queue a -> Queue (a,a)
pairs xs = case view xs of
x :< ys -> case ys of
y :< zs -> (x,y) `cons` pairs zs
_ -> empty
_ -> empty

Well, that's no true nesting since we'd like to write

pairs xs = case view xs of
x :< (y :< zs) -> (x,y) `cons` pairs zs
_ -> empty

but note that we were able to write case ys of instead of the
otherwise obligatory case (view ys) of . With pattern matching on
polymorphic types, real nesting would come in reach. The point is to be
able to define both zip and pairs with one and the same operator :< .


Regards,
apfelmus
Long live the we-want-real-views-or-nothing-at-all movement! :)

[Dan Licata]

Post by apfelmus
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))

That is, the result of the view type is a parameter, so you can
instantiate it with both the viewed type and another view (and so on if
you want more levels).

Then the client code looks like this:

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.

This is a well-known technique in the ML community; see, e.g.,
http://www.cs.cmu.edu/~tom7/papers/wizard.pdf

-Dan

[Benjamin Franksen]

Post by Dan Licata

Post by apfelmus
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 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. Does
this scale to views containing multiple nestable constructors?

It would, of course, be nice to get rid of having to write view2
altogether...

Cheers
Ben

[Dan Licata]

Post by Benjamin Franksen

Post by Dan Licata

Post by apfelmus
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 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.

Post by Benjamin Franksen
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

[apfelmus]

Post by Dan Licata
There's actually a quite simple way of doing this. You make the view
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
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.

Post by Dan Licata
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

[Stefan O'Rear]

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.

Post by Jon Fairbairn
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

[Dan Licata]

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

Post by Stefan O'Rear

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.

Post by Jon Fairbairn
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
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
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Stefan O'Rear]

Post by Dan Licata
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 :)

Post by Dan Licata
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.

Post by Dan Licata
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. :)

Post by Dan Licata
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

Post by Dan Licata

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

[Dan Licata]

Post by Stefan O'Rear

Post by Dan Licata
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

[Stefan O'Rear]

Post by Dan Licata

Post by Stefan O'Rear

Post by Dan Licata
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

[Dan Licata]

With the functional dependency, you can't work with the view datatypes
at all. Once you write

type Typ
data TypView = Unit | Arrow Typ Typ

instance View Typ TypView where
view = ...

you're no longer allowed to take apart a TypView at all!

E.g. you can't write

outUnit :: TypView -> Bool
outUnit Unit = True
outUnit _ = False

because the implicit application of the view function will mean that
outUnit must consume a Typ.

Personally, I'd rather have special syntax in the pattern (-> pat) than
have these global effects on what you can do with certain types.

-Dan

Post by Stefan O'Rear

Post by Dan Licata

Post by Stefan O'Rear

Post by Dan Licata
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
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Stefan O'Rear]

Post by Dan Licata
With the functional dependency, you can't work with the view datatypes
at all. Once you write
type Typ
data TypView = Unit | Arrow Typ Typ
instance View Typ TypView where
view = ...
you're no longer allowed to take apart a TypView at all!

Exactly. And I'm 100% convinced it's a non-issue, since all the
heavyweight view proposals don't allow you to manipulate view objects
*at all*. My approach is no worse.

Post by Dan Licata
E.g. you can't write
outUnit :: TypView -> Bool
outUnit Unit = True
outUnit _ = False
because the implicit application of the view function will mean that
outUnit must consume a Typ.

What would you use it for, anyway? TypView objects don't exist
anywhere except internally in case-expressions.

Post by Dan Licata
Personally, I'd rather have special syntax in the pattern (-> pat) than
have these global effects on what you can do with certain types.

You can only declare the instance for TypView in the same module as
TypView itself, since otherwise it would conflict with the implicit
instance. Therefore, providing an instance is no more "global" than
just renaming the type.

Stefan

[Dan Licata]

Post by apfelmus

Post by Dan Licata
There's actually a quite simple way of doing this. You make the view
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
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

[apfelmus]

Post by Dan Licata

Post by apfelmus
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) = ...

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.

Post by Dan Licata
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

[Dan Licata]

Post by apfelmus
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

[Derek Elkins]

Post by Simon Marlow
Cheers
Ben, member of the we-want-real-views-or-nothing-at-all movement ;-)

Derek, member of the counter-culture,
we-don't-want-real-views-but-nothing-at-all-may-suffice movement.

[Dan Licata]

[I think we should move the rest of this thread to haskell-cafe, since
it's getting long. Note that there have already been some responses on
both lists.]

Hi Claus,

I think that the signature

type Typ
unit :: Typ -> Maybe ()
arrow :: Type -> Maybe (Typ,Typ)

is *wrong* if what you really mean is

type Typ
data TypView = Unit | Arrow Typ Typ
view :: Typ -> TypView

different =/= wrong !-)

No, of course not. All I meant to say is that sometimes you want a
total view, and that a total view should be given a type that says as
much. The latter says this better than the former. On the other hand,
there are lots of circumstances in which you want a partial view, and I
think the (... -> Maybe _) types for those are perfectly appropriate.

That is, if what you mean is that every Typ is either Unit or an Arrow
*and nothing else* then the latter signature should be preferred, as it
makes this fact explicit in the type system.

but that is not what you're saying there at all! you're saying that -within
view 'view' of Typ- Typ is mapped to either Unit or Arrow, if the mapping
is successfull. there can be other views of Typ,

Right, but the only issue here is whether this particular view function
is total or not.

and the types do not guarantee that 'view' itself is exhaustive over
Typ (there can be variants of Typ that 'view' fails to map to
TypView).
in the abstract deconstructor variant, this partiality is explicit in the
types,
in the concrete view type variant, it is hidden from the types, implicit in
the implementation of 'view'.

But by this reasoning, every expression you write should have a Maybe
type, since there's always the possibility of match failure or
non-termination. In Haskell, these effects are always implicit in a
type, so there's no need to add extra summands to account for them.
If you think about the *values* of the returned type, then (1 + Typ *
Typ) is what you want, not ((1 + 1) + (1 + Typ * Typ)).

btw, it might be useful to permit association of abstract types
with abstract deconstructors, so that an extended abstract type
(export) declaration somewhat like
type Typ as unit -> () | arrow -> (Typ,Typ)
tells us (and the compiler) that the abstract patterns in the size
function are exhaustive (or at least as exhaustive as clients of
the abstract type Typ are supposed to be). the proof obligation
would be on the exporter of the abstract type, and any pattern
match failures relating to this should be reported as view failures.
doing so would declare a virtual view type, similar to the concrete
view types used in other examples, so there might be several 'as'
clauses for a single abstract type, declaring separate sets of
exhaustive abstract deconstructors.

Setting aside the "transparent ordinary patterns" feature, I think this
is exactly what you get above:
- the data declaration for TypView corresponds to this "as" declaration
- the view function of type Typ -> TypView can be analyzed for
exhaustiveness using GHC's exhaustiveness checker
- a run-time match failure of view will be reported as such

So I don't think I understand what you're going for here. Could you
explain?

-Dan

[Claus Reinke]

Hi Dan,

Post by Dan Licata
No, of course not. All I meant to say is that sometimes you want a
total view, and that a total view should be given a type that says as
much. The latter says this better than the former. On the other hand,
there are lots of circumstances in which you want a partial view, and I
think the (... -> Maybe _) types for those are perfectly appropriate.

indeed. i was only argueing against the 'wrong', or against the unclear
appeal to the type system (which also appears on the wiki page):

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.

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.

Post by Dan Licata
But by this reasoning, every expression you write should have a Maybe
type, since there's always the possibility of match failure or
non-termination. In Haskell, these effects are always implicit in a
type, so there's no need to add extra summands to account for them.
If you think about the *values* of the returned type, then (1 + Typ *
Typ) is what you want, not ((1 + 1) + (1 + Typ * Typ)).

yes, but we were talking about the subset of partiality due to
failure to accept input, rather than the whole class of partiality
due to failure to produce results. in particular, we were talking
about a syntactically checkable subset of that: exhaustiveness
means checking for a certain set of abstract or concrete patterns
(a function with exhaustive matching can still be partial in results).

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.

others prefer to keep the closed sum types, just use view patterns
to transform between different concrete views. as Connor said,
they will want to avoid the Maybe of treating individual patterns in
isolation, and instead treat complete sets of patterns all the time.

i'm not saying that one is better than the other, i'm saying that i
prefer one of them, and that the appeal to typing is misleading
in the form presented.

Post by Dan Licata
Setting aside the "transparent ordinary patterns" feature, I think this
- the data declaration for TypView corresponds to this "as" declaration
- the view function of type Typ -> TypView can be analyzed for
exhaustiveness using GHC's exhaustiveness checker

but note that the type does not encode or guarantee whether or
not such a check has happened, let alone was successful.

Post by Dan Licata
- a run-time match failure of view will be reported as such

the declaration of virtual views as sets of exhaustive abstract patterns
was indeed meant to provide the same documentation as a concrete
view declaration would give.

Post by Dan Licata
So I don't think I understand what you're going for here. Could you
explain?

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).

claus

[Dan Licata]

Post by Claus Reinke
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).

Post by Claus Reinke
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.

Post by Claus Reinke
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.)

Post by Claus Reinke
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

[Jacques Carette]

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

[Claus Reinke]

Post by Dan Licata
Oh! I had assumed that it was already considered rude to expose a

you mean, as in: head, tail, fromJust, ..?-)

whether exposing or using those is considered rude or not, the type
system has nothing to tell us about their not handling some inputs,
and if you get them from precompiled libraries, you don't see the
compiler warnings, either.

Post by Dan Licata

Post by Claus Reinke
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 was talking about name-based (as in: this is the sum type named List)
vs structural (as in: this is the sum type build from Cons and Nil) typing.
the former hides (in-)exhaustiveness from the type system, the latter
exposes it.

consider the example code below, where the type system catches the
non-exhaustiveness of g, where the sum structure of its parameter is
exposed, but has nothing to say about f, where the sum structure is
hidden behind a type name.

claus

{-# OPTIONS_GHC -fallow-overlapping-instances #-}
{-# OPTIONS_GHC -fglasgow-exts #-}

{- our own, nameless sum type with injection and unpacking -}
infixr :|
data a :| b
data a :< b = Inj a deriving Show

class Inj a b where { inj :: a -> a:<b ; out :: a:<b -> a }
instance Inj a a where { inj a = Inj a ; out (Inj a) = a }
instance Inj a (a:|b) where { inj a = Inj a ; out (Inj a) = a }
instance Inj a b => Inj a (c:|b) where { inj a = Inj a ; out (Inj a) = a }

{- a product type of nested pairs, with selection -}
class Sel a b where sel :: b -> a
instance Sel a a where sel a = a
instance Sel a (a,b) where sel (a,_) = a
instance Sel a b => Sel a (c,b) where sel (_,b) = sel b

{- to match, supply a product of functions covering the sum -}
match :: (Inj x xs, Sel (x->b) fs) => x:<xs -> fs -> b
match x fs = sel fs (out x)

{- example A: nameless sum -}
type Sum = String :| Char :| Bool

g y = match y (\s->s::String,
(\c->c:""
))
-- ,(\b->if b then "1" else "2")))

{- example B: named sum -}
data NamedSum = S String | C Char | B Bool deriving Show

f :: NamedSum -> String
f (S s) = s
f (C c) = c:""
-- f (B b) = if b then "1" else "2"

{- testing -}
main = do
putStrLn $ g (inj "hi" :: String:<Sum)
putStrLn $ f (S "ho" :: NamedSum)
putStrLn $ g (inj 'x' :: Char:<Sum)
putStrLn $ f (C 'y' :: NamedSum)
putStrLn $ g (inj False :: Bool:<Sum)
putStrLn $ f (B True :: NamedSum)

[Dan Licata]

Post by Claus Reinke

Post by Dan Licata

Post by Claus Reinke
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 was talking about name-based (as in: this is the sum type named List)
vs structural (as in: this is the sum type build from Cons and Nil) typing.
the former hides (in-)exhaustiveness from the type system, the latter
exposes it.

I don't think the juxtaposition you're setting up here, between
"name-based" and "structural", is correct. You could just as well
choose the elimination form for "name-based" sum types (i.e., datatypes)
to be an exhaustive case analysis. It just happens that Haskell chooses
to permit non-exhaustive case expressions.

-Dan

[Jon Fairbairn]

Post by Simon Marlow

Simon PJ and I are implementing view patterns, a way of
pattern matching against abstract datatypes, in GHC.

At the risk of being a spoil-sport, I have a somewhat
negative take on view patterns. Not because I think they're
particularly bad, but because I don't think they're
significantly useful enough to warrant adding to the
language, at least if we also have pattern guards.

I wholeheartedly agree.

I'd rather see a slightly different question addressed: how
to permit the definition of overloaded functions using
pattern matching (and I mean pattern matching with exactly
the same syntax as anywhere else). In other words, if I write

Post by Simon Marlow
f [] = e
f (a:b) g a b

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

Post by Simon Marlow
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?


* * *

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.

[Jonathan Cast]

Post by Jon Fairbairn

Post by Simon Marlow

Simon PJ and I are implementing view patterns, a way of
pattern matching against abstract datatypes, in GHC.

At the risk of being a spoil-sport, I have a somewhat
negative take on view patterns. Not because I think they're
particularly bad, but because I don't think they're
significantly useful enough to warrant adding to the
language, at least if we also have pattern guards.

I wholeheartedly agree.
I'd rather see a slightly different question addressed: how
to permit the definition of overloaded functions using
pattern matching (and I mean pattern matching with exactly
the same syntax as anywhere else). In other words, if I write

Post by Simon Marlow
f [] = e
f (a:b) g a b

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

Post by Simon Marlow
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?
* * *
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.

I don't have a formal specification, but I think this does that:

-- | Minimal complete definition: either 'empty', 'unit', and 'append' or '[]'
-- and '(:)' + pattern matching
algebraic class Stream s where
empty :: s t
unit :: t -> s t
append :: s t -> s t -> s t
[] :: s t
(:) :: t -> s t -> s t
empty = []
unit x = x : []
append (x:xn) ys = x : (xn `append` ys)
[] = empty
x : xn = unit x `append` xn

De-sugars into:

data StreamView s t
= []
| (:) t (s t)

data Stream s = Stream{
empty :: forall t. s t,
unit :: forall t. t -> s t,
append :: forall t. t -> s t,
nil :: forall t. s t,
cons :: forall t. t -> s t,
viewStream :: forall t. s t -> StreamView s t}

defaultEmpty s = nil s
defaultUnit s x = cons s x (nil s)
defaultAppend s xn ys = case viewStream s xn of
[] -> ys
x : xn' -> cons s x (defaultAppend s xn' ys)
defaultNil s = empty s
defaultCons s x xn = append s (unit s x) xn

Case evaluation proceeds by case analysis of viewStream.

data List t
= Nil
| Cons t (List t)

instance Stream List where
[] = Nil
(:) = Cons
Nil = []
Cons = (:)

De-sugars into:

streamList = Stream{
empty = defaultEmpty streamList,
unit = defaultUnit streamList,
append = defaultAppend streamList,
nil = Nil,
cons = Cons,
viewStream = \ xn -> case xn of
Nil -> []
Cons x xn -> x : xn}

While

data Tsil t
= Lin
| Snoc (Tsil t) t

instance Stream Tsil where
empty = Lin
unit x = Snoc Lin x
xn `append` Lin = xn
xn `append` Snoc ys y = (xn `append` ys) `Snoc` y
Lin = []
Snoc xn x = flip fix (x, Lin, xn) $ \ loop (x, ys, xn) -> case xn of
Lin -> x : ys
Snoc xn' x' -> loop (x', x : ys, xn')

De-sugars into

streamTsil = Stream{
empty = Lin,
unit = Snoc Lin,
append = \ xn ys -> case ys of
Lin -> xn
Snoc ys' y -> (append streamTsil xn ys') `Snoc` y,
nil = defaultNil streamTsil,
cons = defaultCons streamTsil,
viewStream = \ xn -> case xn of
Lin -> []
Snoc xn' x -> flip fix (x, Lin, xn) $ \ loop (x, ys, xn) -> case xn of
Lin -> x : ys
Snoc xn' x' -> loop (x', cons streamTsil x ys, xn')}

The best part is that you can have multiple data types to a view and multiple
views of a data type, and the fact that pattern-matching proceeds one level
at a time; the worst part is the rather syntactic way e.g. (:) as a
view-constructor is distinguished from (:) as a class method. They can't be
distinguished type-wise (e.g., by a dictionary passing mechanism) because
their types aren't unifiable; I think you'd have to define a tail context
within viewStream and replace (:) with the constructor there only. Or change
the view type to

data StreamView t
= []
| t : StreamView t

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs

[ChrisK]

Post by Jon Fairbairn
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

Post by Simon Marlow
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 (->).

[Jon Fairbairn]

Post by ChrisK

Post by Jon Fairbairn
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

Post by Simon Marlow
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).

Post by ChrisK
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]

Post by Jon Fairbairn

Post by ChrisK

Post by Jon Fairbairn
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

Post by Simon Marlow
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.

Post by Jon Fairbairn
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).

Post by ChrisK
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?

[David Roundy]

Post by Jonathan Cast

Post by Jon Fairbairn

Post by ChrisK
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).

[Aaron Denney]

Post by David Roundy
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++.

[ChrisK]

And the readability is destroyed because you cannot do any type inference in
your head.

If you see

{
Matrix m = ....;
Matrix x = m * y;
...;
}

Then you know very little about the possible types of y since can only conclude
that:

Matrix can be multiplied by one or more types 'sometype' becuase it has one or
more (operator *(sometype x)) methods defined.

And 'y' is either one of these sometypes's or _any_ other class that matches
_any_ single argument constructor of any of those sometypes (except for those
constructors are marked 'explicit').

Now you need to read the header definitions for Matrix and the headers for every
type that can multiply Matrix. Only after that can you say what set of types
the 'y' might be.

Now do this for every argument of every method call and every operator in the code.

This is part of the reason that shops that use C++ often have a long list of
features that must never be used. This is part of the reason that new people
who use C++ are notorious because they produce code that uses too many of C++
features. Code written in arbitrary C++ is unreadable.

Post by Aaron Denney

Post by David Roundy
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++.

[Jon Fairbairn]

Post by ChrisK
And the readability is destroyed because you cannot do any type inference in
your head.
If you see
{
Matrix m = ....;
Matrix x = m * y;
...;
}
Then you know very little about the possible types of y

[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

[David Roundy]

Post by Jon Fairbairn

Post by ChrisK
And the readability is destroyed because you cannot do any type inference in
your head.
If you see
{
Matrix m = ....;
Matrix x = m * y;
...;
}
Then you know very little about the possible types of y

[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

What your suggestion would do would be to make the type inferred for every
pattern-matched function polymorphic, which means that in order to
determine the correctness of a function you'd need to examine all other
modules. Similarly, if you fail to include a type signature in some simple
pattern-matched function in a where clause, adding an import of another
module could make that function fail to compile (with an undeterminable
type error).

This isn't so horrid as C++, but also isn't nearly so beautiful as Haskell.
Admittedly, adding a type signature will make a function verifiably
correct, and avoid any of these ambiguities, but we really like type
inference, and it'd be a shame to introduce code that makes type inference
less powerful.

True, one could always forbid people to use the View class, but that sort
of defeats the purpose, and starts sounding once more like C++, where there
are language features that "shouldn't" be used... but just imagine what
would happen to your type checking, if someone decided that it'd be clever
to use [a] as a view for Integer using a Peano representation? Yikes! (Or
Integer as a view for [a] describing the length?)

Admittedly, havoc would also be wreaked if someone declared [a] to be an
instance of Num, and that's the risk one takes when using type
classes... but that's why it's nice that there is a convenient way to write
code that *doesn't* use type classes.

[Stefan O'Rear]

Post by David Roundy

Post by Jon Fairbairn

Post by ChrisK
And the readability is destroyed because you cannot do any type inference in
your head.
If you see
{
Matrix m = ....;
Matrix x = m * y;
...;
}
Then you know very little about the possible types of y

[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

What your suggestion would do would be to make the type inferred for every
pattern-matched function polymorphic, which means that in order to
determine the correctness of a function you'd need to examine all other
modules. Similarly, if you fail to include a type signature in some simple
pattern-matched function in a where clause, adding an import of another
module could make that function fail to compile (with an undeterminable
type error).

Excuse me? One of the most critical properties of type classes is that
adding new instances can never make old code that uses old instances
stop compiling; the worst you could get is a definition conflict.

Stefan

[David Roundy]

Post by Stefan O'Rear

Post by David Roundy

Post by Jon Fairbairn

Post by ChrisK
And the readability is destroyed because you cannot do any type inference in
your head.
If you see
{
Matrix m = ....;
Matrix x = m * y;
...;
}
Then you know very little about the possible types of y

[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

What your suggestion would do would be to make the type inferred for every
pattern-matched function polymorphic, which means that in order to
determine the correctness of a function you'd need to examine all other
modules. Similarly, if you fail to include a type signature in some simple
pattern-matched function in a where clause, adding an import of another
module could make that function fail to compile (with an undeterminable
type error).

Excuse me? One of the most critical properties of type classes is that
adding new instances can never make old code that uses old instances
stop compiling; the worst you could get is a definition conflict.

I see that I was wrong. I was thinking of something like

foo :: C a => Int -> a
bar :: C a => a -> Int
baz :: Int -> Int

baz = bar . foo

and that this would compile if there was only one instance of class C. But
I see that in fact it will fail to compile regardless, which makes sense.

[ChrisK]

Discussion continues below quoted text...

Post by Stefan O'Rear

Post by David Roundy

Post by Jon Fairbairn

Post by ChrisK
And the readability is destroyed because you cannot do any type inference in
your head.
If you see
{
Matrix m = ....;
Matrix x = m * y;
...;
}
Then you know very little about the possible types of y

[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

What your suggestion would do would be to make the type inferred for every
pattern-matched function polymorphic, which means that in order to
determine the correctness of a function you'd need to examine all other
modules. Similarly, if you fail to include a type signature in some simple
pattern-matched function in a where clause, adding an import of another
module could make that function fail to compile (with an undeterminable
type error).

Excuse me? One of the most critical properties of type classes is that
adding new instances can never make old code that uses old instances
stop compiling; the worst you could get is a definition conflict.
Stefan

That is true, and it is one of of the perfect things about type classes. But
that is not the problem with some of the proposals to make normal syntax
patterns always look for a View inference. The problem is that to read any
pattern match I have to know which View instance was chosen. So each and every
pattern match requires me to run a type checker in my head which draws on all
the View instances which were implicitly imported into the current module. That
adding another invisible instance does not break the code is irrelevant, the
problem is that huge amount of effort it takes the human reader to prove to
herself or himself that any particular pattern match has been correctly understood.

It should require a new syntax to invoke this complexity.

[Jon Fairbairn]

Post by David Roundy

Post by Jon Fairbairn
[snippage] This is all very horrid, but as far as I can tell
what I was proposing wouldn't lead to such a mess, except
possibly via defaulting, which, as the least important
aspect of the idea could easily be abandoned.

What your suggestion would do would be to make the type inferred for every
pattern-matched function polymorphic,

No it wouldn't. I reiterate: constructors would either
belong to a class or to a datatype, so for constructors that
belong to a datatype the situation would be exactly as
before.

It's unfortunate that when I wrote my example I assumed that
everyone would understand that for some classes we would
have defaults (because we already have this: the
constructors for Integer effectively belong to a class and
are defaulted to Integer). I'm now quite convinced that
using defaults together with more general overloaded
constructors would be a mistake, but that's all you've
managed to convince me of!

Yes, there is a problem that importing a class with a
constructor into a scope that declares the same constructor
as a data constructor would cause difficulties (namely the
module would nolonger compile), but aren't they exactly the
same difficulties as when the name in question is just a
function name?

[Conor McBride]

Post by Dan Licata

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)

Post by Dan Licata

Post by Conor McBride
abstract occurrences of the expression from the type.

Oh, I see: you use 'with' as a heuristic for guessing the motive

of the

Post by Dan Licata
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