Examples of Type Application for Infix Operators

TypeApp.markdown

Nested

Showing where types change:

infixr 5 :::
data Nest a = N | a ::: Nest (a, a)

In

type I = Integer

as :: Nest I
as = 100 ::: (10, 20) ::: ((1, 2), (3, 4)) ::: N

the constructor ::: gets used at many different types, I want to be able to present it as

type II   = (I, I)
type IIII = (II, II)

as :: Nest I
as = 100           ::: @I 
     (10,20)       ::: @II
     ((1,2),(3,4)) ::: @IIII N

or

as :: Nest I
as =       100           
 ::: @I    (10,20)
 ::: @II   ((1,2),(3,4))
 ::: @IIII N

or

as :: Nest I
as = 
 100           
 ::: @I
 (10, 20)
 ::: @II
 ((1, 2), (3, 4))
 ::: @IIII 
 N

MonadPlus, Codensity

newtype Codensity :: (k -> Type) -> (Type -> Type) where
  Codensity :: (forall xx. (a -> m xx) -> m xx) -> Codensity m a

From From monoids to near-semirings: the essence of MonadPlus and Alternative

instance MonadPlus m => MonadPlus (Codensity m) where
  mzero :: Codensity m a
  mzero @(Codensity m) = Codensity (\k -> mzero @m)

  mplus :: Codensity m a -> Codensity m a -> Codensity m a
  Codensity p `mplus` @(Codensity m) Codensity q = Codensity (\k -> p k `mplus` @m q k)

Messy typeclasses: only positive and only negative used together

reddit

Only positive in mempty :: Monoid m => m, only negative in (==) :: Eq a => a -> a -> Bool:

mempty == mempty

We can easily annotate which makes it asymmetric

mempty @[_] == mempty
-- or
mempty == mempty @[_]

I like having an obvious right choice. Here it is infix type application in my view

mempty == @[_] mempty

Writing

ifoldMapRep' :: forall r m a. (Representable r, Foldable r, Monoid m) => (Rep r -> a -> m) -> (r a -> m)                                                                                                            
ifoldMapRep' ix xs = fold (tabulate (\(i :: Rep r) -> ix i $ index xs i) :: r m)                                                                                                                                    

as

ifoldMapRep' :: forall r m a. (Representable r, Foldable r, Monoid m) => (Rep r -> a -> m) -> (r a -> m)
ifoldMapRep' ix xs = fold (tabulate ((<*>) @((->) (Rep r)) ix (index xs)) :: r m)

is ugly and annoying, this is far better

ifoldMapRep' :: forall r m a. (Representable r, Foldable r, Monoid m) => (Rep r -> a -> m) -> (r a -> m)
ifoldMapRep' ix xs = fold (tabulate (ix <*> @(Rep r ->) index xs) :: r m)

Very annoying example, I want to apply ind to a type variable,

x = mp @f (`ind` f)

but to do this we change the structure of the expresion

x = mp @f (flip (ind @f) f)

instance (Action act, Semigroup a) => Action (MaybeAct act :: m ·- Option a) where
  (··) :: Option a -> m -> m
  Option Nothing  ·· m = m
  Option (Just a) ·· m = (··) @_ @_ @act a m

http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_DRAFT.pdf is forced to add (id :: r Int -> r Int)

data Rule :: (k -> Type) -> (k -> Type) -> Type where
  (==>) :: lhs a -> rhs a -> Rule lhs rhs

class WildCard exp where
  __ :: exp a

rule_mul :: (WildCard lhs, Num (lhs Int), Num (rhs Int)) => Rule lhs rhs
rule_mul = 0 * __ ==> (id :: r Int -> r Int) 0

We can shorten it or write (0 :: _ Int) but it feels rather unnatural

rule_mul :: (WildCard lhs, Num (lhs Int), Num (rhs Int)) => Rule lhs rhs
rule_mul = 0 * __ ==> id @(_ Int) 0

a more natural placement for the application is

rule_mul :: (WildCard lhs, Num (lhs Int), Num (rhs Int)) => Rule lhs rhs
rule_mul = 0 * __ ==> @_ @Int 0

(==>) should manage its own existential variables

Also this

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

  default
    (==) :: Enum a => a -> a -> Bool
  a == b = fromEnum a == @Int fromEnum b