mbrcknl

Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
  has_type empty t T /\ halts t /\
  match T with
    | TBool  => True
    | TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
    | TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
  end.

mbrcknl

Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
  has_type empty t T /\ halts t /\
  match T with
    | TBool  => True
    | TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
    | TProd T1 T2 => R T1 (tfst t) /\ R T2 (tsnd t)
  end.

mbrcknl

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

import qualified Data.Map as M
import Control.Applicative as A

newtype JObject = JObject (M.Map String Json)
newtype JList = JList [Json]

data Json

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March-April 2015

-- With thanks to Conor McBride (@pigworker) for his lecture series:
-- https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
-- from which I learned most of what I know about Agda, and
-- from which I stole several ideas for this talk.

open import Agda.Primitive using (_⊔_)

mbrcknl

Definition red_split_a {red: red_type} {e: aexp} (ret: red_cexp red a e): red_aexp red e :=
  match ret in red_cexp _ t e return
        (match t return exp_type t -> Type with
           | a => fun e' => red_aexp red e'
           | b => fun _  => unit
         end e)
  with
    | RCNum       n     => RANum   n
    | RCPlus  _ _ a1 a2 => RAPlus  a1 a2
    | RCMinus _ _ a1 a2 => RAMinus a1 a2

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March 2015

open import Agda.Primitive using (_⊔_)

postulate
  String : Set

{-# BUILTIN STRING String #-}

mbrcknl

{-# LANGUAGE ScopedTypeVariables #-}

-- | Solve the r-peg Towers of Hanoi puzzle, using the Frame-Stewart algorithm.

module Hanoi where

import Prelude
  ( Bool(..), Int, Integer, Integral, Eq(..), Ord(..), Ordering(..)
  , error, fst, length, map, otherwise, snd, (+), (++), (-), (*), ($)
  , minimum, head, last

mbrcknl

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ m + n = succ (m + n)

_×_ : ℕ → ℕ → ℕ
zero × n = zero

mbrcknl

data bool : Set where
  tt : bool
  ff : bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n

mbrcknl

Keybase proof

I hereby claim:

• I am mbrcknl on github.
• I am mbrcknl (https://keybase.io/mbrcknl) on keybase.
• I have a public key whose fingerprint is 37B9 11E4 FB0C 3331 D832 1E56 3F92 8682 66EE 73F0

To claim this, I am signing this object: