An alternative to witness values
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:
(Metric "Euclidean") => <term involving measure>for example
dot a b = (Metric "Euclidean") => measure a b
- New keyword similar to "where"
dot a b = measure a b assuming (Metric "Euclidean")
- New keyword similar to "let..in"
dot a b = assume (Metric "Euclidean") in measure a b