The previous post on record syntax reminded me of some 'problems' I had noticed where Haskell and mathematics have a (deep) usage mismatch. First, consider a syntax for other component-wise function application? For example, it would be convenient to have (f,g) @ (x,y) be (f x, g y). In some languages [with dynamic typing], one can even do (f,g) (x,y) :-) Yes, I am aware that this untypeable in Haskell, because polymorphism is straight-jacketed by structural rules. But in mathematics, it is convenient and extremely common to: 1) look at the type a -> b as being a *subtype* of b (though I have never seen it phrased that way in print) 2) to consider every 'natural transformation' available and use it (tuples of functions <-> obvious function on tuples) Seeing a -> b as a subtype of b allows one to take any function f : b -> b -> c (like + ) and 'lift' it to ff : (a -> b) -> (a -> b) -> (a -> c) via the obvious definition ff g h = \x -> f (g x) (h x) This is done routinely in mathematics. The meaning of the expression (sin + cos) should be immediately obvious. Such 'lifting' is used even in first-year calculus courses, but not in Haskell. The "same" phenomenon is what allows one to 'see' that there is an obvious function apply_tuple:: (a->b,c->d) -> (a,c) -> (b,d) so that (f,g) (a,b) only has one possible meaning, if the built-in apply function were to be overloaded. Similarly, there are "obvious" maps apply_T :: T (a->b) -> a -> T b for any datatype constructor T (as has been noticed by all who do 'generic' programming). This means that [f, g, h] x == [f x, g x, h x] but also (in mathematics at least) {f, g, h} x == {f x, g x, h x} where {} denotes a set, and the equality above is extensional equality, and so on. Note that some computer algebra systems use #1 and #2 above all the time to define the operational meaning of a lot of syntactic constructs [where I personally extended the use of such rules in the implementation & operational semantics of Maple]. What hope is there to be able to do something 'similar' in a Haskell-like language? Jacques
On Fri, Jan 28, 2005 at 10:01:33AM -0500, Jacques Carette wrote:
The previous post on record syntax reminded me of some 'problems' I had noticed where Haskell and mathematics have a (deep) usage mismatch.
First, consider a syntax for other component-wise function application? For example, it would be convenient to have (f,g) @ (x,y) be (f x, g y). In some languages [with dynamic typing], one can even do (f,g) (x,y) :-) Yes, I am aware that this untypeable in Haskell, because polymorphism is straight-jacketed by structural rules.
It's not as bad as you think. You can do this: {-# OPTIONS -fglasgow-exts #-} module Apply where class Apply f a b | f -> a, f -> b where apply :: f -> a -> b instance Apply (a -> b) a b where apply f a = f a instance Apply (a1 -> b1, a2 -> b2) (a1, a2) (b1, b2) where apply (f1, f2) (a1, a2) = (f1 a1, f2 a2) instance Apply (a1 -> b1, a2 -> b2, a3 -> b3) (a1, a2, a3) (b1, b2, b3) where apply (f1, f2, f3) (a1, a2, a3) = (f1 a1, f2 a2, f3 a3) And then: *Apply> (succ, pred, show) `apply` (1, 2, ()) (2,1,"()") *Apply> (\x -> 2 * x + 1/2, length) `apply` (10, [1,2,3,4,5]) (20.5,5) Best regards, Tomasz
Tomasz Zielonka <tomasz.zielonka@gmail.com> wrote:
It's not as bad as you think. You can do this:
{-# OPTIONS -fglasgow-exts #-}
module Apply where
class Apply f a b | f -> a, f -> b where apply :: f -> a -> b
instance Apply (a -> b) a b where apply f a = f a
instance Apply (a1 -> b1, a2 -> b2) (a1, a2) (b1, b2) where apply (f1, f2) (a1, a2) = (f1 a1, f2 a2) [snip]
Very nice. But in the scrap-your-boilerplate spirit, it would be nice if one could instead say instance* Apply (T (a -> b)) a b where apply (T f) a = T (f a) where instance* is an instance template, and T is a ``shape functor'' (in the sense of polynomial functors specifying an y of algebra/coalgebra/bialgebra/dialgebra). Or maybe even go for analytic functors (a la Joyal). Well, I guess it's up to me to work out the theory... [based on the work of (at least) Jay, Hinze, Jeuring, Laemmel, Jansson and Peyton-Jones ! ] Jacques
Despite being a fan of generic programming, I have my doubts about this kind of automatic lifting. It works fine in "ordinary mathematics", because there is no fear of confusion - one hardly ever deals with functions as entities in their own right. (Witness "sigma sin(x) dx", involving a term sin(x) and a dummy variable x, rather than the more logical "sigma sin", involving the function.) But in FP, of course, functions are first class citizens. So one may get ambiguities on account of it being reasonable to treat a particular function either as "program" or as "data" - with conflicting outcomes. I don't immediately see a problem with automatic lifting of the first argument of function application, as the original poster wanted, but I have seen a problem in the past with "apposition", or conflation of composition and application. Suppose one wants to streamline notation, so that instead of having to write (f . g) $ x one can write f @ g @ x Here, "@" means either composition or application according to context. It is supposed to be associative, so it isn't the same as normal Haskell $; in particular, f @ g is valid and represents the composition of f and g. You might see it as automatically lifting all "base values" (eg :: Int) to functions (:: () -> Int) and using composition everywhere. The problem arises with higher-order appositions; thrice @ thrice (where thrice = \ f -> f . f . f) might mean either application or composition, and the two are different in this context. Jeremy Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html On Fri, 28 Jan 2005, Jacques Carette wrote:
Tomasz Zielonka <tomasz.zielonka@gmail.com> wrote:
It's not as bad as you think. You can do this:
{-# OPTIONS -fglasgow-exts #-}
module Apply where
class Apply f a b | f -> a, f -> b where apply :: f -> a -> b
instance Apply (a -> b) a b where apply f a = f a
instance Apply (a1 -> b1, a2 -> b2) (a1, a2) (b1, b2) where apply (f1, f2) (a1, a2) = (f1 a1, f2 a2) [snip]
Very nice. But in the scrap-your-boilerplate spirit, it would be nice if one could instead say
instance* Apply (T (a -> b)) a b where apply (T f) a = T (f a)
where instance* is an instance template, and T is a ``shape functor'' (in the sense of polynomial functors specifying an y of algebra/coalgebra/bialgebra/dialgebra). Or maybe even go for analytic functors (a la Joyal).
Well, I guess it's up to me to work out the theory... [based on the work of (at least) Jay, Hinze, Jeuring, Laemmel, Jansson and Peyton-Jones ! ]
Jacques _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On Monday 31 January 2005 04:24, Jeremy Gibbons wrote:
Despite being a fan of generic programming, I have my doubts about this kind of automatic lifting. It works fine in "ordinary mathematics", because there is no fear of confusion - one hardly ever deals with functions as entities in their own right.
May I please beg to differ? When I studied math, things were quite different, at least. I remember whole branches of mathematics completely dedicated to dealing with "functions as entities in their own right". One notable example is Functional Analysis, of which I happen to know a little. And, as far as I remember, we used notation which reflected this, i.e. nobody wrote 'f(x)' when actually they meant just 'f', which is the same as '\x -> f x', which in math is usually written 'x |-> f(x)'.
(Witness "sigma sin(x) dx", involving a term sin(x) and a dummy variable x, rather than the more logical "sigma sin", involving the function.)
The notations for 'integral' and 'differential quotient' stem from a time when dealing with functions as entities in their own right was indeed not yet a common concept in mathematics, i.e. earlier than 1900. BTW, 'sigma sin' is not a function. Ben
Jeremy Gibbons <Jeremy.Gibbons@comlab.ox.ac.uk> wrote in article <Pine.GSO.4.51.0501310314250.3639@abacus.comlab> in gmane.comp.lang.haskell.general:
But in FP, of course, functions are first class citizens. So one may get ambiguities on account of it being reasonable to treat a particular function either as "program" or as "data" - with conflicting outcomes...
Suppose one wants to streamline notation, so that instead of having to write (f . g) $ x one can write f @ g @ x Here, "@" means either composition or application according to context. It is supposed to be associative, so it isn't the same as normal Haskell $; in particular, f @ g is valid and represents the composition of f and g.
Indeed, I've been thinking about such a notation, but one that explicitly specifies whether to treat a function as "program" or "data". Variables like "f" always denote data to start with; such data can be thought of as a program that maps unit to a function. Data can be turned into a program by unquoting it with "," (usually I write "@" for unquotation but you use it for composition already). (Conversely, a program can be turned into data by enclosing it in a pair of quotation brackets "[]", a la Joy; unquotation cancels quotation by the reduction step ,[X] => X.) Now (f . g) $ x in Haskell notation is written ,f @ ,g @ x We also distinguish between ,thrice @ thrice and ,thrice @ ,thrice An advantage of this notation is that it exposes the symmetry between call-by-value and call-by-name evaluation: right-to-left evaluation here corresponds to call-by-value, argument-first evaluation; left-to-right evaluation here corresponds to call-by-name evaluation. I could go on and on about this. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig War crimes will be prosecuted. War criminals will be punished. And it will be no defense to say, "I was just following orders."' George W. Bush, address to the nation, 2003-03-17 http://www.whitehouse.gov/news/releases/2003/03/20030317-7.html
Jacques Carette: ....
Yes, I am aware that this untypeable in Haskell, because polymorphism is straight-jacketed by structural rules. But in mathematics, it is convenient and extremely common to: 1) look at the type a -> b as being a *subtype* of b (though I have never seen it phrased that way in print) 2) to consider every 'natural transformation' available and use it (tuples of functions <-> obvious function on tuples)
Seeing a -> b as a subtype of b allows one to take any function f : b -> b -> c (like + ) and 'lift' it to ff : (a -> b) -> (a -> b) -> (a -> c) via the obvious definition ff g h = \x -> f (g x) (h x) This is done routinely in mathematics. The meaning of the expression (sin + cos) should be immediately obvious. Such 'lifting' is used even in first-year calculus courses, but not in Haskell.
I would like to remark that some array languages are doing this kind of overloading (e.g., A + B means elementwise addition of A and B, when A and B are arrays). If arrays are seen as functions from finite index domains, then this is just a special case of your "math" overloading. Examples of such languages are Fortran 90, HPF, and (the specified, but never implemented) functional language Sisal 2.0. All these languages are first-order, explicitly typed, and provide this overloading only for a predefined set of builtin primitives. However, I think this can be extended to functions in general, in higher-order languages with Hindley-Milner (HM) type inference. I had a PhD student working on this a couple of years ago. Alas, he dropped out before getting his PhD, but we got as far as defining an extended inference system with some nice properties, and I do believe that a reasonable inference algorithm can be found. Rather than using subtyping, this system uses "transformational" judgements of the form A |- e -> e':t, where e':t is inferrable in the original HM type system. Thus, this system resolves the overloading during type inference. For instance, with a proper assumption set A, we would have A |- sin + cos -> (\x -> sin x + cos x). Now, whether you would want to have this overloading unleashed in a higher order language is another matter. I think it can be useful in some contexts, but probably restricted in some way. Also, in Haskell there would be potential conflicts with the overloading provided by the class system (Num being a prime example). Björn Lisper
participants (6)
-
Benjamin Franksen -
Bjorn Lisper -
Chung-chieh Shan -
Jacques Carette -
Jeremy Gibbons -
Tomasz Zielonka