Changes between Version 13 and Version 14 of ExistentialQuantification

Feb 1, 2006 10:43:18 AM (10 years ago)


  • ExistentialQuantification

    v13 v14  
    8787 * The Omega language based on Haskell has an 'exists' keyword to denote an existential type.
     89== Extension: better syntactic support ==
     91Discussion on the list in late January focussed on a [ proposal from Johannes Waldmann] to add syntactic support for the use of existential types.
     93=== Background example ===
     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
     97class Figure f ...
     99with instances `Circle r` and `Rectangle h w`, say. The existential built on the `Figure` class is given by
     101data EFigure = exists f . Figure f => EFigure f
     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:
     105instance Figure EFigure ...
     107but boxing needs to be explicit.
     109=== First proposal ===
     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
     113f :: Integer -> Circle
     114g :: Figure -> Blah
     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
     118f :: Integer -> [Circle]
     119g :: [Figure] -> Blah
     121for instance.
     123=== Consensus proposal: an existential for each single parameter class ===
     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
     127class Figure f ...
     128data Figure = exists f . Figure f => Figure f
     129instance Figure Figure ...
     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.
    90133== Pros ==
    91134 * offered by GHC, Hugs and Nhc98 for years, HBC even longer.