masaeedu

- an adjunction `F -| G`
 - is read "F is left adjoint to G"
 - consist of functors `F : D -> C` and `G : C -> D`
 - gives rise to a monad `GF : D -> D` and a comonad `FG : C -> C`

- adjunctions can be composed
 - consider two adjunctions:
   - `F' -| (G' : D -> E)`
   - `F  -| (G  : C -> D)`

masaeedu

const { cata } = require("@masaeedu/fp")
const { adt, match } = require("@masaeedu/adt")

// All of these are common, reusable utilities you could get from a library
const classes = (() => {
  const foldable = ({ foldMap }) => {
    const fold = fn.flip(foldMap)(fn.identity)
    return { fold }
  }
  const bifoldable = ({ bifoldMap }) => {

masaeedu

module Data.Record.Operations where

import Data.Functor.Variant (SProxy(..))
import Data.Monoid (class Monoid)
import Prim.RowList (Cons, Nil, kind RowList)
import Type.Data.Boolean (True, False, kind Boolean)
import Type.Data.Symbol (class Equals)
import Type.Prelude (class ListToRow, class RowToList)
import Unsafe.Coerce (unsafeCoerce)

masaeedu

module SquishyAppend where

import Prelude

import Data.Functor.Variant (SProxy(..))
import Data.Monoid (class Monoid, class Semigroup, mempty, (<>))
import Data.Tuple (Tuple(..))
import Prim.RowList (Cons, Nil, kind RowList)
import Record as Record
import Type.Data.Boolean (True, False, kind Boolean)

masaeedu

type Whatever
  (c :: k -> Constraint)
  (f :: k -> *)
  (v :: k)
  = forall x. (c v => f v -> x) -> x

class Everything (a :: k)
instance Everything a

foo :: (forall x. (cb b => x) -> (ca a => x), f b -> f a) -> (ca a => f a) -> (cb b => f b)

masaeedu

{-# LANGUAGE
    DataKinds
  , KindSignatures
  , PolyKinds
  , ConstraintKinds

  , GADTs

  , TypeFamilies
  , MultiParamTypeClasses

masaeedu

{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, PolyKinds, TypeOperators, MultiParamTypeClasses, GADTs, FlexibleContexts, AllowAmbiguousTypes #-}

module Rig where

type Hom c = c -> c -> *

-- A (small) category
class GCategory (p :: Hom c)
  where
  gidentity :: forall a. p a a

masaeedu

{-# LANGUAGE RankNTypes, TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeApplications, DuplicateRecordFields, FlexibleContexts, ScopedTypeVariables #-}
module Main where

import Data.IORef
import Control.Monad.Reader
import Control.Monad.State

type (~>) f g = forall x. f x -> g x

newtype Product f g a = Product { runProduct :: (f a, g a) }

masaeedu

{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators #-}

module Traversals where

import Control.Monad.Free

type (~>) f g = forall x. f x -> g x

data Nat = Z | S Nat

masaeedu

module Adjunctions where

data Coproduct n x
  where
  First :: x -> Coproduct 'Z x
  Next :: Either (Coproduct n x) x -> Coproduct ('S n) x

fold :: Coproduct n x -> x
fold (First x) = x
fold (Next (Right x)) = x