Row Types for Type Classes

Row_types.markdown

Type classes in terms of row types

type Semigroup s = { Monoid s with mappend :: s -> s -> s | _ }

type Pointed f = { Applicative f with pure  :: forall a. a -> f a | _ }
type Apply   f = { Applicative f with (<*>) :: forall a b. f (a -> b) -> f a -> f b | _ }
type Bind    m = { Monad       m with (>>=) :: forall a b. m a -> (a -> m b) -> m b | _ }

https://youtu.be/YTaNkWjd-ac?t=3604 Edward wants to split MonadReader and MonadWriter up into algebraic (ask + tell) and non-algebraic.. Edward describes a painful change he's putting off, this on the other hand is fine

type AlgMonadReader r m = { MonadReader r m with ask :: m r | _ }

type AlgMonadWriter w m = { MonadWriter r m with tell :: w -> m () | _ }

Here is a PureScript ticket created by Kmett (purescript/purescript-transformers#63) that proposes this

More info: http://comonad.com/reader/2011/monads-from-comonads/

Sadly this breaks down a little for Writer and Reader as the mtl unfortunately has historically included a bunch of extra baggage in these classes. In particular, in reader, the notion of local isn't always available, blocking some otherwise perfectly good MonadReader instances, and I've chosen not to repeat this mistake in comonad-transformers.

I don't know which is the better formulation...

instance (Monoid a) { mappend } => Monoid (Maybe a) where
  mempty = Nothing

  Nothing `mappend` Nothing = Nothing
  Just a  `mappend` Nothing = Just a
  Nothing `mappend` Just b  = Just b
  Just a  `mappend` Just b  = Just (mappend a b)

or

-- (r / a), for all rows (r) which lack a field (a)
Monoid a / mempty => Monoid (Maybe a)

Monoid a / (mempty :: a) => Monoid (Maybe a)

or taking it completely by label (+ type? namespaced? who knows)

{mappend : a -> a -> a} => Monoid (Maybe a)

{mappend} => Monoid (Maybe a)

{mappend @a} => Monoid (Maybe a)

This would help me make use of Bits default methods

bitDefault :: (Bits a, Num a) => Int -> a 

testBitDefault :: (Bits a, Num a) => a -> Int -> Bool

popCountDefault :: (Bits a, Num a) => a -> Int

whose type could be changed to

bitDefault :: (Bits a with shiftL, Num a) => Int -> a
bitDefault = \i -> 1 `shiftL` i

testBitDefault ::  (Bits a with (bit, (.&.)), Num a) => a -> Int -> Bool
testBitDefault = \x i -> (x .&. bit i) /= 0

popCountDefault :: (Bits a with (.&.), Num a) => a -> Int
popCountDefault = go 0
 where
   go !c 0 = c
   go c w = go (c+1) (w .&. (w - 1))

We can then define a newtype

newtype WrapBits a = WrapBits a 

-- ignoring wrapping
instance (Bits a / bit / testBit / popCount, Num a) => Bits (WrapBits a) where
  bit = bitDefault
  testBit = testBitDefault
  popCount = popCountDefault

  shift = shift
  rotate = rotate
  bitSize = bitSize
  bitSizeMaybe = bitSizeMaybe
  isSigned = isSigned

I suck at row types, maybe a better approach is

type Semigroup s = forall rest. { mappend :: s -> s -> s | rest }

type Pointed f = forall rest. { Functor f, pure :: forall a. a -> f a | rest }
type Apply   f = forall rest. { Functor f, (<*>) :: forall a b. f (a -> b) -> f a -> f b | rest }
type Bind    m = forall rest. { Applicative m, (>>=) :: forall a b. m a -> (a -> m b) -> m b | rest }

More basic example, which emulates MINIMAL or something something (methods defined in terms of other methods)

newtype WrapEq  a = WEq  a
newtype WrapNeq a = WNeq a

instance (Eq a / (/=)) => Eq (WrapEq a) where
  WEq a == WEq b = a == b
  WEq a /= WEq b = not (a == b)

instance (Eq a / (==)) => Eq (WrapNeq a) where
  WNeq a == WNeq b = not (a /= b)
  WNeq a /= WNeq b = a /= b

if Eq were defined as

class Eq a where
  (==) :: a -> a -> a 
  (/=) :: a -> a -> a

type Semigroupoid cat = Category cat / id

type Semigroup a = Monoid a / mempty

instance Semigroupoid cat =>  Semigroup (Join cat a) where
  Join f `mappend` Join g = Join (f . g)

instance Category cat => Monoid (Join cat a) where
  mempty = Join id

How do we distinguish method-less classes? Thinking with newtypes

class Semigroup s where
  (<>) :: s -> s -> s

class Semigroup m => Monoid m where
  mempty :: m

class Monoid g => Group g where
  invert :: g -> g -> g

class Group g => Abelian g

Not ideal but (are we assuming { Monoid g, inverse :: g -> g -> g } dumps everything from Monoid g into scope? does that defeat the purpose)

newtype Semigroup s = Semigroup { (<>) :: s -> s -> s }
  deriving newtype (Has "(<>)")

newtype Monoid m = Monoid { Semigroup m, mempty :: m }
  deriving newtype (Has "(<>)", Has "mempty")

newtype Group g = Group { Monoid g, inverse :: g -> g -> g }
  deriving newtype (Has "(<>)", Has "mempty", Has "inverse")

newtype Abelian g = Abelian (Group g)
  deriving newtype (Has "(<>)", Has "mempty", Has "inverse")

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/scopedlabels.pdf

newtype Semigroupoid :: (k -> k -> Type) -> Constraint where
  Semigroupoid :: Category cat / id -> Semigroupoid cat

class Semigroupoid cat => Category cat where

Hans idea

newtype Semigroupoid cat = Semigroupoid { (.) :: forall b c a. cat b c -> cat a b -> cat a c }

newtype Category cat = Category { id :: forall a. cat a a, Semigroupoid cat }

and separately defined superclass relationship

class Semigroupoid cat => Category cat

id, instance resolution kicks in.. look at things in scope, finds Control.Category.id from Control.Category.Category

id must have type id :: Category cat => cat a a

---

http://openaccess.city.ac.uk/1141/1/Constructors.pdf

data FoldL b a = FoldL (a -> b -> a) a

Although FoldL is not a functor, it nevertheless has operations similar to unit and mult. These can be described using a type class similar to Monoidal, but without the Functor superclass:

class Zip z where 
  zunit :: z ()
  zmult :: z a -> z b -> z (a, b)

consider removing super classes

Type Inference for GADTs and Anti-unification

(==) :: forall a. {(==) : a -> a -> Bool}. a -> a -> Bool

https://twitter.com/nomeata/status/979823045471866881

I believe this could be solved the same way

This is an interesting idea, several ways of expressing this: what is the relationship between Arbitrary and EquivArbitrary

class EquivArbitrary a where
  arbitraryFrom :: Gen (Gen a)
  default
   arbitraryFrom :: Arbitrary a => Gen (Gen a)
  arbitraryFrom = pure arbitrary

class EquivArbitrary a => Arbitrary a where
  arbitrary :: Gen a
  arbitrary = join arbitraryFrom

class Arbitrary a where
  {-# Minimal arbitrary | arbitraryFrom #-}
  arbitrary :: Gen a
  arbitrary = join arbitraryFrom

  arbitraryFrom :: Gen (Gen a)
  arbitraryFrom = pure arbitrary

type NoMult a = Num a - (*) https://twitter.com/bitemyapp/status/986115468133052417

System CT https://ac.els-cdn.com/S1571066105804554/1-s2.0-S1571066105804554-main.pdf?_tid=bbd12dcf-7585-4054-99a5-b65414a04ad4&acdnat=1552447164_798983bc9e0b2f9ac1f6050223781552