Email Gateway (Aug 19 2022 at 14:23): Email Gateway (Aug 19 2022 at 14:23):From: John Wickerson <johnwickerson@cantab.net>
Hi,
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.
Would that work?
Thanks,
John
Email Gateway (Aug 19 2022 at 14:23):From: Christian Sternagel <c.sternagel@gmail.com>
Hi John,
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.
cheers
chris
Email Gateway (Aug 19 2022 at 14:28):From: Makarius <makarius@sketis.net>
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
http://stackoverflow.com/questions/1722726/is-the-scala-2-8-collections-library-a-case-of-the-longest-suicide-note-in-hist
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"
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05115.html
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.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC