raichoo

module Codensity where

open import Level
open import Function

data Codensity {l} (M : Set l → Set l) (A : Set l) : Set (suc l) where
  codensity : ({B : Set l} → (A → M B) → M B) → Codensity M A

runCodensity : ∀ {l} {A : Set l} {M : Set l → Set l}
             → Codensity M A

raichoo

{-# LANGUAGE RankNTypes #-}
module Church where

import Prelude hiding (and, fst, snd, or, either, succ, toInteger)

type Prod a b = forall c. (a -> b -> c) -> c

and :: a -> b -> Prod a b
and x y p = p x y

raichoo

module Main

{-
  Strictness always bothers me a little, since it forces you to do
  things like fusion manually. This prohibits code reuse. I won't
  elaborate on this too much since there is already a great blog
  post about this:

  http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-evaluation-in.html

raichoo

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
module Comonad where

import Prelude (Functor(..))

class Functor m => Monad m where
  return :: a -> m a
  join   :: m (m a) -> m a

raichoo

{-# LANGUAGE PatternSynonyms #-}
module Polynomial where

import Prelude hiding (Maybe(..))

class Bifunctor f where
  bimap :: (a -> b) -> (c -> d) -> f a c -> f b d

instance Bifunctor (,) where
  bimap f g (x, y) = (f x, g y)

raichoo

module Polynomial where

import Prelude hiding (Maybe(..))

class Bifunctor f where
  bimap :: (a -> b) -> (c -> d) -> f a c -> f b d

instance Bifunctor (,) where
  bimap f g (x, y) = (f x, g y)

raichoo

-- This MinList example is taken from the Safe Haskell paper

{-# LANGUAGE Safe #-}
{-# LANGUAGE RoleAnnotations #-}
module MinList (MinList, newMinList, insertMin) where

data MinList a = MinList a [a]
  deriving Show

type role MinList nominal

raichoo

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Main where

import Control.Monad.Free
import Control.Monad.State hiding (withState)

import Data.Functor.Coyoneda
import Data.Char (toUpper)

raichoo

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
module MonadBase where

import Language.Haskell.TH

class (Monad m, Monad t) => MonadBase m t | t -> m where

raichoo

{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NPlusKPatterns #-}
module Main where