[GHC] #9107: An alternative to witness values

[GHC]

#9107: An alternative to witness values
----------------------------------------------+----------------------------
       Reporter:  spacekitteh                 |             Owner:
           Type:  feature request             |            Status:  new
       Priority:  normal                      |         Milestone:
      Component:  Compiler                    |           Version:  7.9
       Keywords:                              |  Operating System:
   Architecture:  Unknown/Multiple            |  Unknown/Multiple
     Difficulty:  Moderate (less than a day)  |   Type of failure:
     Blocked By:                              |  None/Unknown
Related Tickets:                              |         Test Case:
                                              |          Blocking:
----------------------------------------------+----------------------------
 So, I might have come up with a nicer notation to providing type
 witnesses.

 Say I have a class thusly:


 {{{
 class Metric a where
     measure :: Vector f -> Vector f -> f
 }}}


 and an example instance:


 {{{
 instance Metric "Euclidean" where
     measure = sum . (zipWith (*))
 }}}

 In order to actually use a specific metric, one would have to modify the
 type signature to include a witness, and use it such as {{{measure
 undefined::"Euclidean" a b}}}. Personally, I find such expressions to be
 ugly clutter.

 Instead, here are three alternate proposals which don't require including
 a witness:

 1. {{{(Metric "Euclidean") => <term involving measure>}}} for example
 {{{dot a b = (Metric "Euclidean") => measure a b}}}

 2. New keyword similar to "where"
 {{{
  dot a b = measure a b assuming (Metric "Euclidean")
 }}}

 3. New keyword similar to "let..in"
 {{{dot a b = assume (Metric "Euclidean") in measure a b}}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9107>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler