[GHC] #9107: An alternative to witness values

#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

#9107: An alternative to witness values ----------------------------+---------------------------------------------- Reporter: | Owner: spacekitteh | Status: new Type: feature | Milestone: request | Version: 7.9 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Comment (by spacekitteh): Such an extension would appear to be relatively straightforward to implement, by simply adding extra constraints to the typechecker at the call site, and removing the "The class method 'measure' mentions none of the type variables of the class Metric k a" error during compilation of the typeclass. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9107#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9107: An alternative to witness values ----------------------------+---------------------------------------------- Reporter: | Owner: spacekitteh | Status: closed Type: feature | Milestone: request | Version: 7.9 Priority: normal | Keywords: Component: | Architecture: Unknown/Multiple Compiler | Difficulty: Moderate (less than a day) Resolution: invalid | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Changes (by carter): * status: new => closed * resolution: => invalid Comment: This seems to be covered by using either of Implicit Params or Proxy types the Proxy witness type in http://www.haskell.org/ghc/docs/7.8.2/html/libraries/base-4.7.0.0/Data- Proxy.html see http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type- extensions.html for info on implicit parameters closing. Also ask me or others on IRC if stumped about how to use those -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9107#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC