4 ms·

I don't see how that mechanism provides subtyping (which typeclasses do)? Last I checked Haskell's structures weren't structurally typed.

• tel 13y ago
  You could do it like in Agda, data ApplicativeI f = AI { pure :: forall a. a -> f a , ap :: forall a b. f (a -> b) -> f a -> f b , _FunctorI :: FunctorI f } data MonadI m = AI { bind :: forall a b. (a -> m b) -> m a -> m b , _ApplicativeI :: ApplicativeI m } return :: _MonadI m -> a -> m a return (MonadI { _ApplicativeI = ApplicativeI { pure = fn } }) = fn
  • colanderman 13y ago
    Almost, but that's not extensible: I can't declare some new typeclass Foo and then declare that every x s.t. Monad x is also Foo x without editing the definition of Monad.
    • tome 13y ago
      Instead of providing an instance declaration you provide a value of MonadI f -> FooI f.
      • tel 13y ago
        Exactly, and then that function is "proof" of the relationship.