*To*: Christian Sternagel <c.sternagel at gmail.com>, John Wickerson <johnwickerson at cantab.net>*Subject*: Re: [isabelle] map, difference, image, etc.*From*: Makarius <makarius at sketis.net>*Date*: Fri, 2 May 2014 15:28:09 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <53564590.7080002@gmail.com>*References*: <35F0A690-A4E6-46AC-A346-91815D06F379@cantab.net> <53564590.7080002@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 22 Apr 2014, Christian Sternagel wrote:

the type classes of Isabelle are restricted to a single type parameter and donot support constructor classes (i.e., type classes of higher kind).The latter restriction is the reason why your proposal cannot be implementedusing Isabelle's type classes.If it is just about syntax, adhoc overloading would work. However, this canlead to many situations where explicit type constraints have to be added inorder to avoid ambiguity. So I wouldn't go for that.On 04/22/2014 12:23 PM, John Wickerson wrote: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.

Makarius

- Previous by Date: [isabelle] VSTTE CfP (Deadline tomorrow) - no prior abstract submission needed
- Next by Date: [isabelle] PPDP 2014: 2nd Call for Papers
- Previous by Thread: [isabelle] VSTTE CfP (Deadline tomorrow) - no prior abstract submission needed
- Next by Thread: [isabelle] PPDP 2014: 2nd Call for Papers
- Cl-isabelle-users May 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list