gallais

module SemigroupPuzzles where

open import Algebra
open import Function

module _ {c ℓ} (S : Semigroup c ℓ)
       (open Semigroup S)
       (assumption : (e f : Carrier) → e ∙ f ∙ e ≈ e)
       where

gallais

data Extend' (r :: Nat -> *) (t :: *) (n :: Nat) where
  Here  :: t   -> Extend' r t Zero
  There :: r n -> Extend' r t (Succ n)

type family Extend (r :: Nat -> *) (t :: *) (n :: Nat) where
  Extend r t Zero     = t
  Extend r t (Succ n) = r n

gallais

module Primes where

import Control.Monad

primesFrom []     = []
primesFrom (x:xs) = x : primesFrom (filter ((0 /=) . (`mod` x)) xs)

main = do
  let c = primesFrom [2..200]
  print $ length $ do

gallais

module ListCase where

listCase :: (a -> [a] -> b) -> [a] -> [b]
listCase f [] = []
listCase f (x:xs) = f x xs : listCase f xs

paraList :: (a -> [a] -> b -> b) -> b -> [a] -> b
paraList c n []       = n
paraList c n (x : xs) = c x xs $ paraList c n xs

gallais

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE PolyKinds            #-}

module STLC where

-- Defining type and the corresponding singletons

gallais

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ 

infix 40 _+_
_+_ : ℕ → ℕ → ℕ
zero + zero = zero
(suc a) + zero = suc a
zero + (suc b) = suc b
(suc a) + (suc b) = suc (suc (a + b))

gallais

open import Data.Nat
open import Data.Product
open import Data.Vec as Vec

allPairs : {A : Set} {m n : ℕ} -> Vec A m -> Vec A n -> Vec (A × A) (m * n)
allPairs xs ys = Vec.concat (Vec.map (λ x -> Vec.map (λ y -> (x , y)) ys) xs)

infixl 5 _∈xs++_ _∈_++ys _∈map_xs
_∈xs++_ : {A : Set} {x : A} {m : ℕ} {xs : Vec A m} (prx : x ∈ xs) {n : ℕ} (ys : Vec A n) → x ∈ xs ++ ys
here     ∈xs++ ys = here

gallais

{-# LANGUAGE Rank2Types #-}

module MatchFree where

newtype F f a = F { runF :: forall r. (a -> r) -> (f r -> r) -> r }

pureF :: a -> F f a
pureF a = F $ const . ($ a)

freeF :: Functor f => f (F f a) -> F f a

gallais

Inductive Nat := O : Nat | S : Nat -> Nat.
Inductive isSuc : Nat -> Prop := Indeed : forall (n : Nat), isSuc (S n).
Definition diag : Nat -> Prop :=
  fun n =>
  match n with
    | O   => False
    | S _ => True
  end.
Definition invert : isSuc O -> False :=
 fun isSuc0 => isSuc_ind diag (fun _ => I) O isSuc0.

gallais

Require Import List.

Module Currying.
  Record class (Dom : Type) (Curr : Type -> Type) :=
         Class { Fun : forall cod, Curr cod -> (Dom -> cod) }.
  Structure type := Pack { dom      : Type
                         ; curr     : Type -> Type
                         ; class_of : class dom curr }.
  Definition flippedmap (Curry : type) :
    forall cod, list (dom Curry) -> curr Curry cod -> list cod.