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
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)
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
Very annoying example, I want to apply
ind
to a type variable,but to do this we change the structure of the expresion