Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
show how quantifiedconstraints can be used for writing highly polymorphic versions of functions like pure
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall #-}
module MaybeT where
import Control.Monad.Trans
import Data.Coerce
import Data.Proxy
import Unsafe.Coerce
newtype MaybeT m a = MaybeT { unMaybeT :: m (Maybe a) }
-- type role MaybeT representational representational
instance MonadTrans MaybeT where
lift :: Monad m => m a -> MaybeT m a
lift ma = MaybeT $ fmap Just ma
instance Functor m => Functor (MaybeT m) where
fmap :: forall a b. (a -> b) -> MaybeT m a -> MaybeT m b
fmap a2b (MaybeT ma) = MaybeT go
go :: m (Maybe b)
go =
let _ = ma :: m (Maybe a)
in fmap inner ma
inner :: forall anyM. Functor anyM => anyM a -> anyM b
inner = fmap a2b
-- | This instance (and implementation of pure), requires that @m x@ is
-- representationally equal as long as @x@ is representationally equal. In
-- practice, this is too restrictive because we may want to use this Applicative
-- instance with something that is not representationally equal (for instance
-- the MyGADT below).
-- instance (forall x y. Coercible x y => Coercible (m x) (m y), Applicative m) => Applicative (MaybeT m) where
-- pure :: a -> MaybeT m a
-- pure a = pure' (Proxy @Maybe) a
instance Applicative m => Applicative (MaybeT m) where
pure :: a -> MaybeT m a
pure a = MaybeT $ pure (pure a)
(<*>) :: forall a b. MaybeT m (a -> b) -> MaybeT m a -> MaybeT m b
MaybeT ma2b <*> MaybeT ma = MaybeT go
go :: m (Maybe b)
go =
let _ = ma2b :: m (Maybe (a -> b))
_ = ma :: m (Maybe a)
in inner <$> ma2b <*> ma
inner :: forall anyM. Applicative anyM => anyM (a -> b) -> anyM a -> anyM b
inner = (<*>)
-- | This is a generic version of pure that will work for both EitherT and MaybeT.
:: forall a m inner proxy n
. ( Applicative m
, Applicative inner
-- This says that as long as for all x and y that are representationally
-- equal, we know that (m (inner x)) and (n m y) are representationally
-- equal. This is exactly what we need to be able to do the coersion.
-- However, I think this will NOT work if @m@ is a GADT, since the type-role
-- of @a@ in @m a@ may not be representational in that case.
, forall x y. Coercible x y => Coercible (m (inner x)) (n m y)
=> proxy inner
-> a
-> n m a
pure' _ a = coerce (pure (pure a) :: m (inner a))
-- | This is similar to 'pure'', but it is using unsafeCoerce, so it is less
-- safe.
pure'' :: forall a n m inner proxy. (Applicative inner, Applicative m) => proxy inner -> a -> n m a
pure'' _ a = unsafeCoerce (pure (pure a) :: m (inner a))
newtype EitherT e m a = EitherT { unEitherT :: m (Either e a) }
data MyGADT a where
Pure :: a -> MyGADT a
Intiii :: Int -> MyGADT Int
type role MyGADT nominal
instance Functor MyGADT where
fmap :: (a -> b) -> MyGADT a -> MyGADT b
fmap a2b (Pure a) = Pure (a2b a)
fmap i2b (Intiii i) = Pure (i2b i)
instance Applicative MyGADT where
pure = Pure
(<*>) :: MyGADT (a -> b) -> MyGADT a -> MyGADT b
Pure a2b <*> Pure a = Pure (a2b a)
Pure i2b <*> Intiii i = Pure (i2b i)
blah :: MaybeT MyGADT String
blah = pure "hello"
-- blah = MaybeT (Pure (Just "hello"))

This comment has been minimized.

Copy link
Owner Author

@cdepillabout cdepillabout commented Apr 11, 2019

This will of course only run in GHC-8.6 or greater because it is using QuantifiedConstraints.

This QuantifiedConstraint trick comes from here:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment