Changes between Version 13 and Version 14 of ExistentialQuantification


Ignore:
Timestamp:
Feb 1, 2006 10:43:18 AM (8 years ago)
Author:
s.j.thompson@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExistentialQuantification

    v13 v14  
    8787 * The Omega language based on Haskell has an 'exists' keyword to denote an existential type. 
    8888 
    89   
     89== Extension: better syntactic support == 
     90 
     91Discussion on the list in late January focussed on a [http://www.haskell.org//pipermail/haskell-cafe/2005-June/010516.html proposal from Johannes Waldmann] to add syntactic support for the use of existential types.  
     92 
     93=== Background example === 
     94 
     95The status quo is illustrated by the concrete example of geometrical figures, each of which is an instance of an interface given by the Haskell class 
     96{{{ 
     97class Figure f ... 
     98}}} 
     99with instances `Circle r` and `Rectangle h w`, say. The existential built on the `Figure` class is given by  
     100{{{ 
     101data EFigure = exists f . Figure f => EFigure f 
     102}}} 
     103Elements of this type have the form `EFigure (Circle r)` and so the values of the existential type are explicitly 'boxed' by the `EFigure` constructor when they are built and need to be unboxed when they are used. Unboxing can be achieved by an additional instance declaration: 
     104{{{ 
     105instance Figure EFigure ... 
     106}}} 
     107but boxing needs to be explicit. 
     108 
     109=== First proposal === 
     110 
     111The extension proposed here is to hide the existence of the data type and constructor `EFigure`, just referring to `Figure` instead. The issue becomes one of conversion between the figure types `Circle` and `Rectangle` and the type `Figure`. A concrete example is given by 
     112{{{ 
     113f :: Integer -> Circle 
     114g :: Figure -> Blah 
     115}}} 
     116in order for the expression `g . f` to be well typed, a conversion needs to be inserted thus: `g . EFigure . f`. Conversions become more complicated in case that 
     117{{{ 
     118f :: Integer -> [Circle] 
     119g :: [Figure] -> Blah 
     120}}} 
     121for instance.  
     122 
     123=== Consensus proposal: an existential for each single parameter class === 
     124 
     125The consensus proposal based on the discussion is automatically to introduce an existential type for each single parameter type class. The type and class would have the same name, as in 
     126{{{ 
     127class Figure f ... 
     128data Figure = exists f . Figure f => Figure f 
     129instance Figure Figure ... 
     130}}} 
     131Discussion focussed on whether there should or should not be automatic conversion from figure types into `Figure`; it was agreed that the `Figure` constructor could be used to do this, with the `Figure` instance providing the unboxing required. 
     132 
    90133== Pros == 
    91134 * offered by GHC, Hugs and Nhc98 for years, HBC even longer.