jozefg

This is my short-ish tutorial on how to implement closures in
a simple functional language: Foo.

First, some boilerplate.

> {-# LANGUAGE DeriveFunctor, TypeFamilies #-}
> import Control.Applicative
> import Control.Monad.Gen
> import Control.Monad.Writer
> import Data.Functor.Foldable

jozefg

module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data Tm : ℕ → Set where
  var   : ∀ {n} → F.Fin n → Tm n

jozefg

#!/usr/bin/env python3
from datetime import date, timedelta
import argparse
import time
import itertools

import requests
import feedparser

OKBLUE = '\033[94m'

jozefg

module cantor where
open import Data.Product
open import Data.Empty
open import Level

-- A variant of (https://coq.inria.fr/refman/language/core/inductive.html?highlight=cantor)

-- Sort of spooky this works.
data _≡_ {ℓ : Level}{A : Set ℓ} : A → A → Set₀ where
  refl : (a : A) → a ≡ a

jozefg

signature TYPEINFER =
sig
    type tvar =  int
    datatype monotype = TBool
                      | TArr of monotype * monotype
                      | TVar of tvar
    datatype polytype = PolyType of int list * monotype
    datatype exp = True
                 | False
                 | Var of int

jozefg

module Syn =
  struct
    type uni_level = int
    type t =
      | Var of int (* DeBruijn indices for variables *)
      | Nat | Zero | Suc of t | NRec of t * t * t * t
      | Pi of t * t | Lam of t | Ap of t * t
      | Uni of uni_level
      | Subst of t * subst
     and subst =

jozefg

open import Data.Product
open import Relation.Binary.PropositionalEquality

singleton-contractible : {A : Set}(x : A) (p : Σ[ y ∈ A ] x ≡ y) → (x , refl) ≡ p
singleton-contractible x ( .x , refl )= refl

transport : {A : Set}(B : A → Set)(x y : A) → x ≡ y → B x → B y
transport B x .x refl b = b

J : {A : Set}(B : (x y : A) → x ≡ y → Set) → ((x : A) → B x x refl) → (x y : A)(p : x ≡ y) → B x y p

jozefg

\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{pftools}

\@ifundefined{basedir}{%
\RequirePackage{locallabel}
}{%
\RequirePackage{\basedir locallabel}
}%

\RequirePackage{Tabbing}	% Avoid the standard tabbing environment. Its \< conflicts with the semantic package.

jozefg

;; auctex is under the name auctex on elpa but provides
;; the symbol tex. No clue why..
(require-package 'auctex 'tex)
(require-package 'reftex)
(require-package 'auctex-latexmk)

(setq TeX-auto-save t)
(setq TeX-parse-self t)
(setq-default TeX-engine 'default)
(add-hook 'LaTeX-mode-hook 'turn-on-reftex)

jozefg

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
module Tail where

type CL a = forall c. (a -> c -> c) -> c -> c

t :: CL a  -> (forall c. (a -> (Bool -> c) -> (Bool -> c))
               -> (Bool -> c)
               -> (Bool -> c))
t fold cons nil = fold myCons myNil