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
andType
- 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 onceLocalModules
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 toclass
es in that case - we could just as well allowinstance
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