
123

On Jul25, Benjamin Franksen wrote:
> Dan Licata wrote:
> > On Jul25, apfelmus wrote:
> >> The point is to be
> >> able to define both zip and pairs with one and the same operator :< .
> >
> > There's actually a quite simple way of doing this. You make the view
> > type polymorphic, but not in the way you did:
> >
> > type Queue elt
> > empty :: Queue elt
> > cons :: elt > Queue elt > Queue elt
> >
> > data ViewL elt rec = EmptyL
> >  elt :< rec
> >
> > view :: Queue elt > ViewL elt (Queue elt)
> > view2 :: Queue elt > ViewL elt (ViewL elt (Queue elt))
>
> This is cool! The more so because 'view2' can quite easily be defined in
> terms of 'view'
>
> view2 q = case view q of
> EmptyL > EmptyL
> x :< q' > x :< view q'
>
> so it suffices to provide the onelevel 'view' as a library function.
Right. The way I usually do it is to define, e.g.,
viewGen :: (Queue elt > a) > Queue elt > ViewL elt a
 expose one level, applying the input to the subterms
And then externally you can define
view :: Queue elt > ViewL elt (Queue elt)
view = viewGen id
view2 :: Queue elt > ViewL elt (ViewL elt (Queue elt))
view2 = viewGen view
etc.
> Does this scale to views containing multiple nestable constructors?
I'm not sure quite what you mean? Multiple datatype constructors,
rather than just 2? Certainly. Multiple mutually recursive types? Yes,
but you need one parameter to each view type for each type in the loop.
The main limitation is that you have to program in a style where you
first define the deep view function that you need and then you use it.
This is somewhat syntactically inconvenient if you have a lot of "view"
idioms that you only use once or twice. Of course, then you can just go
back to stringing out the cases.
Dan
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


Dan Licata wrote:
> There's actually a quite simple way of doing this. You make the view
> type polymorphic, but not in the way you did:
>
> myzip :: Queue a > Queue b > Queue (a,b)
> myzip a b = case (view a, view b) of
> (EmptyL, _) > empty
> (_, EmptyL) > empty
> (h1 :< t1, h2 :< t2) > (h1,h2) `cons` myzip a b
>
> pairs :: Queue a > Queue (a,a)
> pairs a = case view2 a of
> h1 :< (h2 :< t) > (h1, h2) `cons` pairs t
> _ > empty
>
> The only difference with view patterns is that you can do the view2
> inside the pattern itself:
>
> pairs (view2 > h1 :< (h2 :< t)) = (h1,h2) `cons` pairs t
> pairs _ = empty
>
> This would be useful if the thing you were viewing were deep inside
> another pattern.
Well, the main feature of view patterns is that you can nest them. In
other words, the canonical way of writing pairs would be
pairs (view > h1 :< (view > h2 :< t)) = (h1,h2) `cons` pairs t
pairs _ = empty
Nesting means to decide "later" on how to pattern match the nested part.
With view2, you have to make this decision before, something I want to
avoid.
For example, take the (silly) definition
foo :: Queue a > Queue a
foo xs = case view xs of
x :< (y :< zs) > x `cons` zs
x :< ys > ys
EmptyL > empty
Here, ys is a Queue and (y :< zs) is a ViewL. By scrutinizing xs
via view , both have to be a Queue. By scrutinizing it via view2 ,
both have to be a ViewL. But I want to mix them.
The idea is to introduce a new language extension, namely the ability to
pattern match a polymorphic type. For demonstration, let
class ViewInt a where
view :: Integer > a
instance ViewInt [Bool] where
view n = ...  binary representation
data Nat = Zero  Succ Nat
instance ViewInt Nat where
view n = ...  representation as peano number
be some views of the integers. Now, I'd like to be able to write
bar :: (forall a . ViewInt a => a) > String
bar Zero = ...
bar (True:xs) = ...
Here, the patterns have different types but the key is that is
unproblematic since the polymorphic type is capable of unifying with
each one.
Given this language extension, we can make foo a valid definition by
using a polymorphic type as the second component of :<
data ViewL = EmptyL  Integer :< (forall a . ViewInt a => a)
In the end, the doublenegation translation
Integer
=> (forall a . ViewInt a => a)
can even be done implicitly and for all types. Together with the magic
class View, this would give real views.
Jón Fairbairn wrote:
> It's essential to this idea that it doesn't involve any new
> pattern matching syntax; the meaning of pattern matching for
> overloaded functions should be just as transparent as for
> nonoverloaded 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Wed, Jul 25, 2007 at 09:35:32PM +0200, apfelmus wrote:
> Integer
> => (forall a . ViewInt a => a)
>
> can even be done implicitly and for all types. Together with the magic
> class View, this would give real views.
>
>
> Jón Fairbairn wrote:
> > It's essential to this idea that it doesn't involve any new
> > pattern matching syntax; the meaning of pattern matching for
> > overloaded functions should be just as transparent as for
> > nonoverloaded 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
fnoimplicitprelude) we have:
class View a c  c > a where
view :: a > c
and we provide a derivingform 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 nonbinding identifiers in patterns!
Stefan
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Jul25, apfelmus wrote:
> Dan Licata wrote:
> > There's actually a quite simple way of doing this. You make the view
> > type polymorphic, but not in the way you did:
> >
> > myzip :: Queue a > Queue b > Queue (a,b)
> > myzip a b = case (view a, view b) of
> > (EmptyL, _) > empty
> > (_, EmptyL) > empty
> > (h1 :< t1, h2 :< t2) > (h1,h2) `cons` myzip a b
> >
> > pairs :: Queue a > Queue (a,a)
> > pairs a = case view2 a of
> > h1 :< (h2 :< t) > (h1, h2) `cons` pairs t
> > _ > empty
> >
> > The only difference with view patterns is that you can do the view2
> > inside the pattern itself:
> >
> > pairs (view2 > h1 :< (h2 :< t)) = (h1,h2) `cons` pairs t
> > pairs _ = empty
> >
> > This would be useful if the thing you were viewing were deep inside
> > another pattern.
>
> Well, the main feature of view patterns is that you can nest them. In
> other words, the canonical way of writing pairs would be
>
> pairs (view > h1 :< (view > h2 :< t)) = (h1,h2) `cons` pairs t
> pairs _ = empty
>
> Nesting means to decide "later" on how to pattern match the nested part.
> With view2, you have to make this decision before, something I want to
> avoid.
>
> For example, take the (silly) definition
>
> foo :: Queue a > Queue a
> foo xs = case view xs of
> x :< (y :< zs) > x `cons` zs
> x :< ys > ys
> EmptyL > empty
>
> Here, ys is a Queue and (y :< zs) is a ViewL. By scrutinizing xs
> via view , both have to be a Queue. By scrutinizing it via view2 ,
> both have to be a ViewL. But I want to mix them.
>
> The idea is to introduce a new language extension, namely the ability to
> pattern match a polymorphic type. For demonstration, let
>
> class ViewInt a where
> view :: Integer > a
>
> instance ViewInt [Bool] where
> view n = ...  binary representation
>
> data Nat = Zero  Succ Nat
>
> instance ViewInt Nat where
> view n = ...  representation as peano number
>
> be some views of the integers. Now, I'd like to be able to write
>
> bar :: (forall a . ViewInt a => a) > String
> bar Zero = ...
> bar (True:xs) = ...
This doesn't make sense to me:
Zero :: Nat
and therefore
Zero :: ViewInt Nat => Nat
but you can't generalize from that to
Zero :: forall a. ViewInt a => a
E.g., Zero does not have type ViewInt [Bool] => Bool
Maybe you wanted an existential instead, and what you're writing is
sugar for
bar :: (exists a . ViewInt a => a) > String
bar (pack[Nat](view[Nat] > Zero)) = ...
bar (pack[Bool List](view[Bool List] > True:xs)) = ...
(where I'm using [] to make the polymorphic instantiations clear).
That is, you open the existential, and then use the view function at the
the unpacked type in each case and match against the result.
Note that matching against types like this is a form of intensional type
analysis.
Dan
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Jul25, Claus Reinke wrote:
> although you could introduce a _convention_ by which all view functions
> are supposed to be exhaustive over their input type, the types themselves
> do not encode or check exhaustiveness. so we're talking about an informal
> promise rather than a formal guarantee.
Oh! I had assumed that it was already considered rude to expose a
nonexhaustive 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 lambdamatch stuff on the Haskell' list. So how
can a client use such a function? Either he has to do a check first (if
canCallF x then f x else ...) or he has to know for other reasons that
the precondition holds. In either case, it seems like the right thing
to do is to encode the precondition in the type system (if only using
abstract types, so the implementation of the module is still
unverified).
> one could turn that promise into a typechecked guarantee by using
> explicit sum types (and thus structural rather than namebased typing),
> but that gets awkward in plain haskell.
I don't think the choice of whether you label your variants with names
or with numbers (in1, in2, in3...) has anything to do with the choice of
whether you require your cases to be exhaustive or not.
> i often feel limited by the nonextensible, needtobenamed 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/nontermination.)
> 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 firstclass patterns or my library support and examples
> for lambdamatch on the haskellprime 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


Jon Fairbairn wrote:
> I currently only get f :: [t] > something, so if I later
> discover that I need to change the input representation to
> be more efficient than lists, I have to rewrite f. Wouldn't
> it be so much nicer if I could simply add a declaration
>
>> f:: Stream s => s t > something
>
> and get a function that works on anything in the Stream
> class?
>
> The core of the idea would be to allow classes to include
> constructors (and associated destructors) so the definition
> of Stream would include something for ":" and "[]" and their
> inverses, though I've no real idea of the details; can
> anyone come up with a plan?
I had been avoiding adding my two cents, but I must object to this.
Because this is starting to sound like one of the maddening things about C++.
Namely, the automatic implicit casting conversions of classes via their single
argument constructors. This is one of the (several) things that makes reading
and understanding a function or method call in C++ incredibly difficult.
What if the 'f' in the quoted message above is itself part of a type class.
Then one has to decide which instance 'f' is being called and what
constructors/destructors are being called to view the 's t' parameter as the
correct concrete type. That way lies madness.
Any magical view logic is dangerous in this respect. Thus I would probably not
want any special implicit (class View a b) or (call View a b  a > b), etc.
At least the proposal that (=> _) is (> Just _) makes you change the syntax
instead of overloading (>).

Chris
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


Hi Dan
On 25 Jul 2007, at 15:18, Dan Licata wrote:
> Hi Conor,
>
[..]
> Why are you so fatalistic about "with" in Haskell?
I guess I'm just fatalistic, generally. Plausibility is not something
I'm especially talented at.
> Is it harder to
> implement than it looks?
For Haskell, it ought to be very easy.
> It seems to be roughly in the same category as
> our view pattern proposal, in that it's just an addition to the syntax
> of pattern matching, and it has a straightforward elaboration into the
> internal language.
Even on the source level, the withblocks just expand as "helper
functions". I wonder if I have the time and energy to knock up a
preprocessor...
> (Well, for Haskell it's more straightforward than
> for Epigram, because we don't need to construct the evidence for
> ruling
> out contradictory branches, etc., necessary to translate to inductive
> family elims.)
In the dependently typed setting, it's often the case that the
"withscrutinee" 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 typelevel computation tide.
All the best
Conor
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


Dan Licata wrote:
> apfelmus wrote:
>> The idea is to introduce a new language extension, namely the ability to
>> pattern match a polymorphic type. For demonstration, let
>>
>> class ViewInt a where
>> view :: Integer > a
>>
>> instance ViewInt [Bool] where
>> view n = ...  binary representation
>>
>> data Nat = Zero  Succ Nat
>>
>> instance ViewInt Nat where
>> view n = ...  representation as peano number
>>
>> be some views of the integers. Now, I'd like to be able to write
>>
>> bar :: (forall a . ViewInt a => a) > String
>> bar Zero = ...
>> bar (True:xs) = ...
>
> This doesn't make sense to me:
>
> Zero :: Nat
>
> and therefore
>
> Zero :: ViewInt Nat => Nat
>
> but you can't generalize from that to
>
> Zero :: forall a. ViewInt a => a
>
> E.g., Zero does not have type ViewInt [Bool] => Bool
Yes, the types of the patterns don't unify. But each one is a
specialization of the argument type. Note that the type signature is
bar :: (forall a . ViewInt a => a) > String
which is very different from
bar :: forall a . ViewInt a => a > String
Without the extension, we would write bar as follows
bar :: (forall a . ViewInt a => a) > String
bar x = let xNat = x :: Nat in
case xNat of
Zero > ...
_ > let xListBool = x :: [Bool] in
case xListBool of
True:xs > ...
In other words, we can specialize the polymorphic argument to each
pattern type and each equation may match successfully.
> Maybe you wanted an existential instead
No. That would indeed mean to pick the matching equation by analysing
the packed type, i.e. some equations don't match since their patterns
have the wrong type. I think that such a thing violates parametricity.
Regards,
apfelmus
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


> In the dependently typed setting, it's often the case that the
> "withscrutinee" 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
withscrutinee 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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 nonfunctional type class will make everything very polymorphic
(e.g., where we used to infer a type based on the datatype constructors
that occurred, we will now say that it's anything that can be viewed as
that datatype).
So, this syntax affects a lot of code, existing or otherwise, that
doesn't use view patterns, which is something we're trying to avoid.
Dan
On Jul25, Stefan O'Rear wrote:
> On Wed, Jul 25, 2007 at 09:35:32PM +0200, apfelmus wrote:
> > Integer
> > => (forall a . ViewInt a => a)
> >
> > can even be done implicitly and for all types. Together with the magic
> > class View, this would give real views.
> >
> >
> > Jón Fairbairn wrote:
> > > It's essential to this idea that it doesn't involve any new
> > > pattern matching syntax; the meaning of pattern matching for
> > > overloaded functions should be just as transparent as for
> > > nonoverloaded 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
> fnoimplicitprelude) we have:
>
> class View a c  c > a where
> view :: a > c
>
> and we provide a derivingform 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 nonbinding identifiers in patterns!
>
> Stefan
> _______________________________________________
> HaskellCafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskellcafe_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Thu, Jul 26, 2007 at 11:28:03AM 0400, Dan Licata wrote:
> I think what you're describing is equivalent to making the "implicit
> view function" syntax so terse that you don't write anything at all. So
> the pattern 'p' is always (view > p).
Thanks, I wouldn't have thought of such a simple explanation myself :)
> This seems like a pretty invasive change:
>
> I don't think the version with the functional dependency works (unless
> you adopt some form of scoped type class instances, as you suggest
> below), because then if you want to use a datatype as a view, you can no
> longer pattern match on the datatype itself at all! Even with some form
> of scoping, you can't decompose the view datatype as itself and as a
> view in the same scope.
Right, you can't pattern match on a type that is used as a view. But
from what I've seen in library code, that usually doesn't happen 
nobody matches ViewL except with viewl in the scrutinee, etc. You could
create a proxy type (at some cost in ugliness) in the cases where you
want to use the same structure for a concrete type and a view.
> The nonfunctional type class will make everything very polymorphic
> (e.g., where we used to infer a type based on the datatype constructors
> that occurred, we will now say that it's anything that can be viewed as
> that datatype).
That's exactly the typing problem that I ... no wait I didn't actually
mention it. :)
> So, this syntax affects a lot of code, existing or otherwise, that
> doesn't use view patterns, which is something we're trying to avoid.
Eh? I *think* the typing rules are the same for the noview case. If
the autoderiving hack isn't implemented, you only need a
deriving(View), otherwise there should be no change at all...
Stefan
> > It's possible to go even simpler, and implement views via a simple
> > desugaring without altering the typechecking kernel at all.
> >
> > (for simplicity of exposition, assume pattern matches have already been
> > compiled to flat cases using Johnsson's algorithm; in particular the
> > patterns mentioned consist of exactly one constructor, not zero)
> >
> > case scrut of
> > pat > a
> > _ > b
> >
> > ==>
> >
> > realcase (Prelude.view scrut) of
> > pat > a
> > _ > b
> >
> > Where in the Prelude (or the current type environment, if
> > fnoimplicitprelude) we have:
> >
> > class View a c  c > a where
> > view :: a > c
> >
> > and we provide a derivingform 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 nonbinding identifiers in patterns!
> >
> > Stefan
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Jul26, Stefan O'Rear wrote:
> > So, this syntax affects a lot of code, existing or otherwise, that
> > doesn't use view patterns, which is something we're trying to avoid.
>
> Eh? I *think* the typing rules are the same for the noview case. If
> the autoderiving 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Jul26, apfelmus wrote:
> Yes, the types of the patterns don't unify. But each one is a
> specialization of the argument type. Note that the type signature is
>
> bar :: (forall a . ViewInt a => a) > String
>
> which is very different from
>
> bar :: forall a . ViewInt a => a > String
>
> Without the extension, we would write bar as follows
>
> bar :: (forall a . ViewInt a => a) > String
> bar x = let xNat = x :: Nat in
> case xNat of
> Zero > ...
> _ > let xListBool = x :: [Bool] in
> case xListBool of
> True:xs > ...
>
> In other words, we can specialize the polymorphic argument to each
> pattern type and each equation may match successfully.
Oh, I understand what you're saying now. Thanks for clarifying!
Dan
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


Me:
> > In the dependently typed setting, it's often the case that the
> > "withscrutinee" is an expression of interest precisely because it
> > occurs
> > in the *type* of the function being defined. Correspondingly, an
> > Epigram implementation should (and the Agda 2 implementation now
does)
> > abstract occurrences of the expression from the type.
Dan:
> Oh, I see: you use 'with' as a heuristic for guessing the motive
of the
> inductive family elim. How do you pick which occurrences of the
> withscrutinee 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'
Lefthand 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 lefthand
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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


ChrisK < [hidden email]> writes:
> Jon Fairbairn wrote:
> > I currently only get f :: [t] > something, so if I later
> > discover that I need to change the input representation to
> > be more efficient than lists, I have to rewrite f. Wouldn't
> > it be so much nicer if I could simply add a declaration
> >
> >> f:: Stream s => s t > something
> > and get a function that works on anything in the Stream
> > class?
> > The core of the idea would be to allow classes to include
> > constructors (and associated destructors) so the definition
> > of Stream would include something for ":" and "[]" and their
> > inverses, though I've no real idea of the details; can
> > anyone come up with a plan?
>
> I had been avoiding adding my two cents, but I must object to this.
>
> Because this is starting to sound like one of the
> maddening things about C++.
>
> Namely, the automatic implicit casting conversions of
> classes via their single argument constructors.
Unfortunately I'm not sufficiently familiar with C++ to know
what this means. Perhaps you could clarify?
Despite the obvious interpretation of my message (ahem), I'm
not advocating much that's automatic. In the case of lists I
was imagining that they would be the default for Streams in
much the same way that Integer is the default for Num. I'd
be happy to discard that part of the idea (though I'd expect
howls of protest from those who want lists to be ruling
class citizens).
> What if the 'f' in the quoted message above is itself part
> of a type class. Then one has to decide which instance 'f'
> is being called and what constructors/destructors are being
> called to view the 's t' parameter as the correct concrete
> type. That way lies madness.
Again, I think the difficulty here is a discrepancy between
the interpretation of what I wrote and what I intended to
mean :), viz that classes could (in addition to their usual
functions) define constructor/deconstructor pairs that would
be used in desugaring pattern matching. I didn't mean that
constructors of the same name could appear both in classes
and in data declarations. So if one had something like
class Stream s where
Cons:: a > s a > s a
Nil:: s a
Snoc:: s a > a > s a
...
{ an instance definition for Stream would have to
somehow give both construction and deconstruction
functions for Cons and Nil }
then a definition of the form
f Nil = ...
f (Cons h t) = ...
would be unambiguously f:: Stream s => s a > ... (in the
absence of defaulting). There are issues about checking
coverage of cases, but I don't think that's the problem you
were raising?

Jón Fairbairn [hidden email]
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Friday 27 July 2007, Jon Fairbairn wrote:
> ChrisK < [hidden email]> writes:
> > Jon Fairbairn wrote:
> > > I currently only get f :: [t] > something, so if I later
> > > discover that I need to change the input representation to
> > > be more efficient than lists, I have to rewrite f. Wouldn't
> > > it be so much nicer if I could simply add a declaration
> > >
> > >> f:: Stream s => s t > something
> > >
> > > and get a function that works on anything in the Stream
> > > class?
> > > The core of the idea would be to allow classes to include
> > > constructors (and associated destructors) so the definition
> > > of Stream would include something for ":" and "[]" and their
> > > inverses, though I've no real idea of the details; can
> > > anyone come up with a plan?
> >
> > I had been avoiding adding my two cents, but I must object to this.
> >
> > Because this is starting to sound like one of the
> > maddening things about C++.
> >
> > Namely, the automatic implicit casting conversions of
> > classes via their single argument constructors.
>
> Unfortunately I'm not sufficiently familiar with C++ to know
> what this means. Perhaps you could clarify?
Somebody noticed that, in C, you could mix integers and floats (almost)
freely, and in Classic C, you could mix pointers and integers freely, and
thought this was /such/ a wonderful idea that C++ has special syntax to
declare the conversion functions allowing you to, say, mix pointers and
pointerlike 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);
Typecheck.
> Despite the obvious interpretation of my message (ahem), I'm
> not advocating much that's automatic. In the case of lists I
> was imagining that they would be the default for Streams in
> much the same way that Integer is the default for Num. I'd
> be happy to discard that part of the idea (though I'd expect
> howls of protest from those who want lists to be ruling
> class citizens).
>
> > What if the 'f' in the quoted message above is itself part
> > of a type class. Then one has to decide which instance 'f'
> > is being called and what constructors/destructors are being
> > called to view the 's t' parameter as the correct concrete
> > type. That way lies madness.
>
> Again, I think the difficulty here is a discrepancy between
> the interpretation of what I wrote and what I intended to
> mean :), viz that classes could (in addition to their usual
> functions) define constructor/deconstructor pairs that would
> be used in desugaring pattern matching. I didn't mean that
> constructors of the same name could appear both in classes
> and in data declarations. So if one had something like
>
> class Stream s where
> Cons:: a > s a > s a
> Nil:: s a
> Snoc:: s a > a > s a
> ...
>
> { an instance definition for Stream would have to
> somehow give both construction and deconstruction
> functions for Cons and Nil }
>
> then a definition of the form
>
> f Nil = ...
> f (Cons h t) = ...
>
> would be unambiguously f:: Stream s => s a > ... (in the
> absence of defaulting). There are issues about checking
> coverage of cases, but I don't think that's the problem you
> were raising?

Jonathan Cast
http://sourceforge.net/projects/fidcorehttp://sourceforge.net/projects/fidemacs_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Fri, Jul 27, 2007 at 05:22:37AM 0400, Dan Licata wrote:
> On Jul26, Stefan O'Rear wrote:
> > > So, this syntax affects a lot of code, existing or otherwise, that
> > > doesn't use view patterns, which is something we're trying to avoid.
> >
> > Eh? I *think* the typing rules are the same for the noview case. If
> > the autoderiving 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 autoderiving 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Fri, Jul 27, 2007 at 09:02:42AM 0500, Jonathan Cast wrote:
> On Friday 27 July 2007, Jon Fairbairn wrote:
> > ChrisK < [hidden email]> writes:
> > > Because this is starting to sound like one of the
> > > maddening things about C++.
> > >
> > > Namely, the automatic implicit casting conversions of
> > > classes via their single argument constructors.
> >
> > Unfortunately I'm not sufficiently familiar with C++ to know
> > what this means. Perhaps you could clarify?
>
> Somebody noticed that, in C, you could mix integers and floats (almost)
> freely, and in Classic C, you could mix pointers and integers freely, and
> thought this was /such/ a wonderful idea that C++ has special syntax to
> declare the conversion functions allowing you to, say, mix pointers and
> pointerlike 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 multipliedalmost 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 singleargument
constructors (except perhaps occasionally when you actually want explicit
construction of objects).
The reasoning behind this, of course, is to allow nice interactions of
homemade classes such as complex numbers, or string classes (which you
might want to be automatically constructed from string constants).

David Roundy
Department of Physics
Oregon State University
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 20070727, David Roundy < [hidden email]> wrote:
> The solution is to add explicit to the constructor for all singleargument
> constructors (except perhaps occasionally when you actually want explicit
> construction of objects).
>
> The reasoning behind this, of course, is to allow nice interactions of
> homemade classes such as complex numbers, or string classes (which you
> might want to be automatically constructed from string constants).
I'd have thought that adding an "implicit" keyword would make more
sense, and only do conversions then. But I forget, C++.

Aaron Denney
><
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe

123
