Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
show how quantifiedconstraints can be used for writing highly polymorphic versions of functions like pure
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# 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
where
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
where
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.
pure'
:: 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"))
@cdepillabout

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:
https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-us-put-join-back-in-monad/

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