First class instances - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

@TheMatten Ah, I just noticed Inst isn't actually parametrized by the type variables of the class

Asad Saeeduddin

Dope:

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)
Asad Saeeduddin

lol

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 (*>) (<*)
Asad Saeeduddin
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 }) t@(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
Asad Saeeduddin

typeclasses rekt forever

TheMatten

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:
instance Foo a = 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:

class Group a where
  unit :: a
  (<>) :: a -> a -> a
  inverse :: a -> a

implement clashing instances as named values

sumRational, prodRational :: Group Rational
sumRational = Group{
    unit = 0
  , (<>) = (+)
  , inverse = negate
  }
prodRational = Group{
    unit = 1
  , (<>) = (*)
  , inverse = (1 /)
  }

and "open" them in scope where needed

foo = 1 <> 2 where Group{..} = prodRational

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...
This is an alternative to #205 that appears to be more compositional. Rendered
Georgi Lyubenov // googleson78

this is also very similar to what agda does

TheMatten

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

@Georgi Lyubenov // googleson78 that's where

"open"

comes from :wink:

Georgi Lyubenov // googleson78

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

TheMatten

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

Georgi Lyubenov // googleson78

https://github.com/ghc-proposals/ghc-proposals/pull/378
maybe I was a bit too pessimistic? @TheMatten

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 #...
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:

Georgi Lyubenov // googleson78

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