gallais

let factorial n =
  let rec loop n k = match n with
    | 0 -> k 1
    | n -> loop (n-1) (fun v -> k (v * n)) in
  loop n (fun x -> x)

gallais

{-# LANGUAGE RankNTypes #-}

module List where

import Data.Monoid

newtype List a = Abstr {
  apply :: forall z . (Monoid z) => (a -> z) -> z
  }

gallais

module Partition where

import Data.Function.Memoize

type Target = Int
type Digits = Int
type MaxInt = Int

partitionMaxBrute :: Digits -> Target -> MaxInt -> [[Int]]
partitionMaxBrute d t m

gallais

{-# LANGUAGE MagicHash #-}

module Word8Mod where

import GHC.Prim
import GHC.Word

f :: Word8 -> Word8 -> Word8
f (W8# x#) (W8# y#) =
  let z# = plusWord# x# y#

gallais

{-# LANGUAGE ScopedTypeVariables #-}

module PowerSet where

import Data.Bits
import GHC.Word

-- Here we want to define the powerset of a list xs "in one go"
-- using the masks corresponding to the binary representations
-- of the numbers between 0 and 2 ^ length xs - 1.

gallais

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ReverseVec where

data Nat = Z | S Nat

gallais

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE OverloadedStrings #-}

module Phantom.Alternative where

-- | universe of validation types
data Validated   = Validated
data Unvalidated = Unvalidated

newtype FormData a = MkFD { pfd :: (Maybe String, String) }

gallais

module Unfold where

newtype Fix f = InFix { outFix :: f (Fix f) }

unfoldFix :: Functor f => (s -> f s) -> s -> Fix f
unfoldFix node = go
  where go = InFix . fmap go . node

data ListF a r = LNil | LCons a r
data TreeF a r = TNil | TLeaf a | TBranch r r

gallais

module tfix where

open import Data.Unit
open import Data.Product

data Desc : Set₁ where
  arg : (A : Set) (d : A → Desc) → Desc
  rec : (r : Desc) → Desc
  ret : Desc

gallais

module Url where

-- We usually start something about TT with the definition
-- of ℕ. So here we go:

data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

-- Now we want to embed a url in the comments. Why not use a