Composing Cofree Comonads

An introduction to PureScript

https://purescript.org

Marcin Szamotulski, PhD

PureScript type system

part i

PureScript

A strongly-typed functional programming language that compiles to JavaScript

Heavily inspired by Haskell.

• Type inference
• Records and row polymorphism
• Newtypes and type aliases
• Polymorphic types
• Higher-kinded types
• Rank N Types
• Multi-parameter type classes & constrained types
• Functional dependencies
• Kind system with kind inference

Records

data Record :: # Type -> Type

a :: Record ( a :: Int, b :: String )
a = { a: 1, b: "" }

b :: { a :: Int, b :: String }
b = { a: 2, b: "a" }

-- in psci
>:k { a :: Int, b :: String }
Type
>:k ( a :: Int, b :: String )
# Type

Row polymorphism

extensible records

add :: forall r. Int -> { a :: Int | r } - { a :: Int | r }
add x r@{ a }  = r { a = a + x}

• rows are association list from labels to types
• rows can have duplicate labels
• unification of rows ignores order of different labels, but preserves order of duplicates

• row of k is a new kind for every kind 
  k

Row polymorphism

extensible effects

main
  :: forall e
   . Eff
      ( console :: CONSOLE
      , http :: HTTP
      , fs :: FS
      , buffer :: BUFFER
      , avar :: AVAR
      , redox :: RedoxStore
        ( read :: ReadRedox
        , write :: WriteRedox
        , subscribe :: SubscribeRedox
        , create :: CreateRedox )
      | e )
  Unit
main = do
  log "starting..."
  store <- mkStore initialState
  runServer defaultOptionsWithLogging {} (app store)

Ranked N Types

foreign import data Exists :: (Type -> Type) -> Type

mkExists :: forall f a. f a -> Exists f
mkExists = unsafeCoerce

runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r
runExists = unsafeCoerce

Multi-parameter Type Classes

class Monad m <= MonadState s m where
  get :: m s
  put :: s -> m Unit

Functional Dependencies

class RowToList
        (row :: # Type)
        (list :: RowList)
        | row -> list

type level prolog

data Z
data S n

class Succ n m | m -> n
instance succInst :: Succ x (S x)

class Pred n m | m -> n
instance predInst :: (Succ x y) => Pred y x

class Gt x y
instance gtpp :: (Pred x xp, Pred y yp, Gt xp yp) => Gt x y
instance gt :: Gt (S x) Z

Composing Cofree interpreters

part ii

Free monad

definition

data Free f a
  = Pure a 
  | Free f (Free f a)

derive instance functorFree :: Functor (Free f)

instance bindFree :: Bind (Free f) where
bind (Pure a) f = f a
bind (Free m) f = (Free (f <$> m))

instance applyFree :: Apply (Free f) where
apply = ap

instance applicativeFree :: Applicative (Free f) where
pure a = Pure a

instance monadFree :: Monad (Free f)

Comonad

definition

-- | Associativity: `extend f <<< extend g = extend (f <<< extend g)`
class Functor w <= Extend w where

-- | Forwards co-Kleisli composition.
composeCoKleisli
  :: forall b a w c
   . Extend w
  => (w a -> b)
  -> (w b -> c)
  -> w a -> c
composeCoKleisli f g w = g (f <<= w)

-- | Duplicate a comonadic context.
duplicate
  :: forall a w
   . Extend w
  => w a -> w (w a)
duplicate = extend id

-- | Left Identity: `extract <<= xs = xs`
-- | Right Identity: `extract (f <<= xs) = f xs`
class Extend w <= Comonad w where
  extract :: forall a. w a -> a

Stream Comonad

data Stream a = Cons a (Lazy (Stream a))

derive instance functorStream :: Functor Stream

instance extendStream :: Extend Stream where
extend f s@(Cons a r) = Cons (f s) (extend f <$> r)

instance comonadStream :: Comonad Stream where
extract (Cons a _) = a

smooth :: Int -> Stream Number -> Stream Number
smooth n s = extend (avN n) s
  where
    sumN :: Int -> Stream Number -> Number
    sumN 0 _ = 0.0
    sumN n (Cons a r) = a + (sumN (n - 1) (force r))

    avN :: Int -> Stream Number -> Number
    avN n s = (sumN n s) / (toNumber n)

Cofree comonad

data Cofree f a = Cofree a (Lazy (f (Cofree f a)))

mkCofree :: forall f a. a -> f (Cofree f a) -> Cofree f a
mkCofree a t = Cofree a (defer \_ -> t)

infixr 5 mkCofree as :<

-- | Returns the label for a tree.
head :: forall f a. Cofree f a -> a
head (Cofree h _) = h

instance functorCofree :: Functor f => Functor (Cofree f) where
map f = loop where
  loop fa@(Cofree head _tail)
    = Cofree (f head) ((map loop) <$> _tail)

instance extendCofree :: Functor f => Extend (Cofree f) where
extend f = loop
  where
    loop fa@(Cofree _ _tail)
      = Cofree (f fa) ((map loop) <$> _tail)

instance comonadCofree :: Functor f => Comonad (Cofree f) where
  extract = head

Composing interpreters

live demo

unfoldCofree
  :: forall f s a
  . Functor f
  => (s -> a)
  -> (s -> f s)
  -> s
  -> Cofree f a
unfoldCofree e n s =
  Cofree (e s) (defer \_ -> unfoldCofree e n <$> n s)

explore
  :: forall f g a b
  . Functor f
  => Functor g
  => (forall x y. f (x -> y) -> g x -> y)
  -> Free f (a -> b)
  -> Cofree g a
  -> b
explore pair m w =
  case runState (runFreeM step m) w of
    Tuple f cof -> f (extract cof)
  where
    step
      :: f (Free f (a -> b))
      -> State (Cofree g a) (Free f (a -> b))
    step ff = state \cof -> pair (map Tuple ff) (tail cof)

newtype Coproduct f g a = Coproduct (Either (f a) (g a))

-- | Left injection
left :: forall f g a. f a -> Coproduct f g a
left fa = Coproduct (Left fa)

-- | Right injection
right :: forall f g a. g a -> Coproduct f g a
right ga = Coproduct (Right ga)

newtype Product f g a = Product (Tuple (f a) (g a))

-- | Create a product.
product :: forall f g a. f a -> g a -> Product f g a
product fa ga = Product (Tuple fa ga)

-- | Returns the label for a tree.
head :: forall f a. Cofree f a -> a
head (Cofree h _) = h

-- | Returns the "subtrees" of a tree.
tail :: forall f a. Cofree f a -> f (Cofree f a)
tail (Cofree _ t) = force t

mkCofree :: forall f a. a -> f (Cofree f a) -> Cofree f a
mkCofree a t = Cofree a (defer \_ -> t)

Composing Streams

live demo

Thank You

written with purescript-smolder and reveal.js