Re: [isabelle] map, difference, image, etc.

On Tue, 22 Apr 2014, Christian Sternagel wrote:

the type classes of Isabelle are restricted to a single type parameter and do not support constructor classes (i.e., type classes of higher kind).

The latter restriction is the reason why your proposal cannot be implemented using Isabelle's type classes.

If it is just about syntax, adhoc overloading would work. However, this can lead to many situations where explicit type constraints have to be added in order to avoid ambiguity. So I wouldn't go for that.

On 04/22/2014 12:23 PM, John Wickerson wrote:

 I recently improved my life quite a lot by assigning an infix operator
 symbol to the ‘map’ function. Expressions like “map (f x) (g y)” could
 become expressions like “f x ``` g y” -- much more readable without all
 those parentheses. As you can see, I chose (```) as my infix operator.

 But it got me thinking: why can’t I just use (`) instead? That is, the
 same symbol as is used for the image of a set. “Map” and “image” are
 pretty similar functions, after all:

 map : (‘a => ‘b) => ‘a list => ‘b list
 image: (‘a => ‘b) => ‘a set => ‘b set

 There’s no problem with (+) being polymorphic over any sort of number, so
 why can’t (`) be polymorphic over any sort of “collection”? And while
 we’re at it, we could make the set-minus operator (-) polymorphic too, so
 that when X and Y are of type “list”, then “X-Y” is the list obtained by
 removing from X all elements in Y.

Just a side-remark: Scala has this insanely complex type-system that can do everything, if you know how it works. There are probably only a handful of people who do. E.g. see the discussion about "map" in the Scala library

The type-system of HOL is much less exciting, just a reduced version of the ML type-system, with the addition of plain-old type classes from original Haskell, before that became very complex in other ways.

Recently, I am often glad about that refreshing simplicity of both HOL and ML. As can be seen on the isabelle-dev thread "Unresponsive Isabelle/jEdit" at the extremely compact Scala notation can lead to bad surprises, when unintended combinators are added by the compiler, and the critical difference is hardly seen in the source text.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.