Consider the following wishful program.
{-# LANGUAGE ExtensibleGADTs #-}
data Free a where
Lift :: a -> Free a
data Free (f a) => FreeFunctor f a where
Map :: (a -> b) -> FreeFunctor f a -> FreeFunctor f b
instance Functor (FreeFunctor f) where
fmap = Map
data FreeFunctor f a => FreeApplicative f a where
Apply :: FreeApplicative f (a -> b) -> FreeApplicative f a -> FreeApplicative f b
Pure :: a -> FreeApplicative f a
instance Applicative (FreeApplicative f) where
(<*>) = Apply
pure = Pure
data FreeApplicative m a => FreeMonad m a where
Bind :: FreeMonad m a -> (a -> FreeMonad m b) -> FreeMonad m b
instance Monad (FreeMonad m) where
(>>=) = Bind
This would introduce a notion of substitutability. For example, a FreeApplicative f a can be substituted by a FreeFunctor f a but not a FreeMonad f a. Similarly, a FreeApplicative f a -> Int can be substituted by a FreeMonad f a -> Int but not a FreeFunctor f a -> Int.
The notion of subtyping can be captured using injections.
import Unsafe.Coerce
fromFreeToFreeFunctor :: Free (f a) -> FreeFunctor f a
fromFreeToFreeFunctor = unsafeCoerce
fromFreeFunctorToFreeApplicative :: FreeFunctor f a -> FreeApplicative f a
fromFreeFunctorToFreeApplicative = unsafeCoerce
fromFreeApplicativeToFreeMonad :: FreeApplicative m a -> FreeMonad m a
fromFreeApplicativeToFreeMonad = unsafeCoerce
The compiler would insert these injections as and where required.
I think that this is a good solution to the expression problem. However, the general consensus is that subtype polymorphism would be problematic in Haskell. So, my question is two fold.
- Would subtyping, as I described above, be problematic or interfere with type inference in Haskell?
- Would extensible GADTs be a viable solution to the expression problem in Haskell?
I haven't defined a precise semantics for extensible GADTs yet. If this seems like something worth pursuing then I'd like to write a GHC extension for this. Just wanted to put this idea out in the wild and get some criticism.