Are extensible GADTs a viable solution to the expression problem?

Viewed 128

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.

  1. Would subtyping, as I described above, be problematic or interfere with type inference in Haskell?
  2. 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.

0 Answers
Related