gallais

{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE RankNTypes          #-}

module MutuallyDefined where

import Data.Type.Natural

gallais

{-# OPTIONS --no-termination-check --no-positivity-check #-}

module MutuallyDefined where

open import Data.Nat as ℕ
open import Data.Fin 
open import Function

data Tie {n : ℕ} (F : (Fin n → Set) → Fin n → Set) (k : Fin n) : Set where
  ⟨_⟩ : (v : F (Tie F) k) → Tie F k

gallais

{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE RankNTypes          #-}

module MutuallyDefinedList where

gallais

module reornament where

open import Data.Product
open import Data.Nat
open import Data.List

ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)

data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where

gallais

Inductive Vector (A : Type) : nat -> Type :=
  | nil  : Vector A O
  | cons : forall n, A -> Vector A n -> Vector A (S n).

Definition head (A : Type) (n : nat) (v : Vector A (S n)) : A.
refine (
  (match v in Vector _ m return m = S n -> A with
   | nil          => _
   | cons _ hd tl => fun _ => hd
  end) (eq_refl (S n))).

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.