type f ~> g = forall x. f x -> g x
data f ~⋅~> g = MMorph
{ convert :: Inst (Monad f) -> Inst (Monad g)
, nat :: f ~> g
}
mapTeletype :: (f ~⋅~> g) -> Inst (Teletype f) -> Inst (Teletype g)
mapTeletype (MMorph { convert, nat }) (Teletype m r w) = Teletype (convert m) (nat r) (nat . w)

ezmonad :: forall m. (forall a b. m a -> (a -> m b) -> m b) -> (forall a. a -> m a) -> Inst (Monad m)
ezmonad (>>=) pure = Monad applicative (>>=) (*>) pure error
where
(<$>) :: (a -> b) -> m a -> m b
(<$>) f ma = ma >>= (pure . f)
($>) :: b -> m a -> m b
($>) = (<$>) . const
functor :: Inst (Functor m)
functor = Functor (<$>) ($>)
(<*>) :: m (a -> b) -> m a -> m b
(<*>) mab ma = mab >>= \ab -> ma >>= \a -> pure $ ab a
liftA2 :: (a -> b -> c) -> m a -> m b -> m c
liftA2 abc fa fb = abc <$> fa <*> fb
(*>) :: m a -> m b -> m b
(*>) ma mb = (flip const) <$> ma <*> mb
(<*) :: m a -> m b -> m a
(<*) ma mb = const <$> ma <*> mb
applicative :: Inst (Applicative m)
applicative = Applicative functor pure (<*>) liftA2 (*>) (<*)

type f ~> g = forall x. f x -> g x
data f ~⋅~> g = MMorph
{ convert :: Inst (Monad f) -> Inst (Monad g)
, nat :: Monad f => f ~> g
}
class Monad m => Teletype m where
read :: m String
write :: String -> m ()
mkInst ''Teletype
mapTeletype :: (f ~⋅~> g) -> Inst (Teletype f) -> Inst (Teletype g)
mapTeletype (MMorph { convert, nat }) [email protected](Teletype m r w) = t ==> Teletype (convert m) (nat r) (nat . w)
newtype ReaderT r m a = ReaderT { runReaderT :: r -> m a }
monadReaderT :: forall r m. Inst (Monad m) -> Inst (Monad (ReaderT r m))
monadReaderT m = m ==> ezmonad (>>=′) pure'
where
(>>=′) :: Monad m => (::>>=) (ReaderT r m)
(ReaderT ma) >>=′ ((runReaderT .) -> amb) = ReaderT $ \r -> ma r >>= ($ r) . amb
pure' :: Monad m => Pure (ReaderT r m)
pure' = ReaderT . pure . pure
liftReaderT :: m ~⋅~> ReaderT r m
liftReaderT = MMorph monadReaderT (ReaderT . pure)
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
monadStateT :: forall s m. Inst (Monad m) -> Inst (Monad (StateT s m))
monadStateT m = m ==> ezmonad (>>=′) pure'
where
(>>=′) :: Monad m => (::>>=) (StateT s m)
(StateT ma) >>=′ ((runStateT .) -> amb) = StateT $ \s -> ma s >>= \(a, s') -> amb a s'
pure' :: Monad m => Pure (StateT s m)
pure' a = StateT $ \s -> pure (a, s)
liftStateT :: m ~⋅~> StateT s m
liftStateT = MMorph monadStateT (\ma -> StateT $ \s -> (, s) <$> ma)
test :: Inst (Teletype f) -> Inst (Teletype (ReaderT r (StateT s f)))
test = mapTeletype liftReaderT . mapTeletype liftStateT

Thinking about this library, way typeclasses work in Haskell and experiences like https://stackoverflow.com/a/25880674, maybe the solution that would allow for best of both worlds would be something along the lines of:

keeping instance creation to the compiler - that is, no (endorsed/safe) way of reifying instances at random places

unifying Constraint and Type - not only we would allow classes to be treated as datatypes, but we would additionally allow users to treat them as normal records, thus removing need for boilerplate needed to make interface usable both implicitly and explicitly (namespacing of newly introduced fields could be solved once LocalModules get implemented)

providing (already proposed) syntax for creating instances from values:

instanceFooa=bar

which allows users to reuse and generate interfaces in convenient way (avoiding tricks with DerivingVia and stuff), while still keeping everything coherent

When it comes to use-cases like multiple instances of numerical interfaces, in presence of functionality above, I would propose simple solution - RecordWildCards:
One could create class that provides needed operations:

If wanted interface contains more methods than class provides, one could use solution that's already used for this purpose with normal values - PatternSynonyms

I once asked a question on haskell beginners, whether to use data/newtype or a typeclass. In my particular case it turned out that no typeclass was required. Additionally Tom Ellis gave me a brilli...

Technically, it wouldn't even make much sense to keep instances restricted to classes in that case - we could just as well allow instances of any datatype as long as they follow normal restrictions

This proposal describes the tension between two important criteria the committee (and broader community) have implicitly been using to evaluate new features. In several proposals (#270, #281, and #...

@rae's thesis was literally about Dependent types in Haskell, and he's paid to work on GHC, so I guess it's just a matter of few years maximum :big_smile:

@TheMatten Ah, I just noticed

`Inst`

isn't actually parametrized by the type variables of the classDope:

lol

typeclasses rekt forever

Thinking about this library, way typeclasses work in Haskell and experiences like https://stackoverflow.com/a/25880674, maybe the solution that would allow for best of both worlds would be something along the lines of:

`Constraint`

and`Type`

- not only we would allow classes to be treated as datatypes, but we would additionally allow users to treat them as normal records, thus removing need for boilerplate needed to make interface usable both implicitly and explicitly (namespacing of newly introduced fields could be solved once`LocalModules`

get implemented)which allows users to reuse and generate interfaces in convenient way (avoiding tricks with

`DerivingVia`

and stuff), while still keeping everything coherentWhen it comes to use-cases like multiple instances of numerical interfaces, in presence of functionality above, I would propose simple solution -

`RecordWildCards`

:One could create class that provides needed operations:

implement clashing instances as named values

and "open" them in scope where needed

If wanted interface contains more methods than class provides, one could use solution that's already used for this purpose with normal values -

`PatternSynonyms`

this is also very similar to what agda does

Technically, it wouldn't even make much sense to keep

`instance`

s restricted to`class`

es in that case - we could just as well allow`instance`

s of any datatype as long as they follow normal restrictions@Georgi Lyubenov // googleson78 that's where

comes from :wink:

if you make a proposal now, maybe my (potential) grandchildren could benefit from it!

:sob:

Pinging @Asad Saeeduddin, because you have bunch of experience with passing dictionaries around, not only in Haskell :smile:

https://github.com/ghc-proposals/ghc-proposals/pull/378

maybe I was a bit too pessimistic? @TheMatten

@rae's thesis was literally about Dependent types in Haskell, and he's paid to work on GHC, so I guess it's just a matter of few years maximum :big_smile:

I was referencing more the fact that ghc hq might actually shift into "more drastic changes" mode