scott-fleischman

module Grammar.Greek.Smyth where

open import Data.Char
open import Data.Maybe
open import Relation.Nullary using (¬_)

-- Smyth §§C,D
data Dialect : Set where
  Aeolic : Dialect -- Aeolic means Lesbian Aeolic; Alcaeus, Saphho; Theocritus idylls
  Boeotian : Dialect -- Aeolic with "many Doric ingredients"

scott-fleischman

module Proof where

data Or {a b} (A : Set a) (B : Set b) : Set₁ where
  Inl : A → Or A B
  Inr : B → Or A B

data And {a b} (A : Set a) (B : Set b) : Set₁ where
  AndIntro : A → B → And A B

and-dist-over-or : {a b c : Set} → And a (Or b c) → Or (And a b) (And a c)

scott-fleischman

data Letter = L_α | L_β | L_γ | L_δ | L_ε | L_ζ | L_η | L_θ | L_ι | L_κ | L_λ | L_μ | L_ν | L_ξ | L_ο | L_π | L_ρ | L_σ | L_τ | L_υ | L_φ | L_χ | L_ψ | L_ω
  deriving (Eq, Show, Ord, Data, Typeable)
data Consonant = C_β | C_γ | C_δ | C_ζ | C_θ | C_κ | C_λ | C_μ | C_ν | C_ξ | C_π | C_ρ | C_σ | C_τ | C_φ | C_χ | C_ψ
  deriving (Eq, Show, Ord, Data, Typeable)
data RoughBreathing = R_῾
  deriving (Eq, Show, Ord, Data, Typeable)
data Vowel = V_α | V_ε | V_η | V_ι | V_ο | V_υ | V_ω
  deriving (Eq, Show, Ord, Data, Typeable)
data Diphthong = D_αι | D_ει | D_οι | D_αυ | D_ευ | D_ου | D_ηυ | D_ωυ | D_υι
  deriving (Eq, Show, Ord, Data, Typeable)

scott-fleischman

• AST editor
  • Variable entry/rename
  • Create fresh variable name
  • \ = lambda
  • space = apply
  • letters = variable
• Show/hide unnecessary parentheses
• Tree view?
• Hover over variables shows binding
• Maybe free variables of the same name or shadowed ones are highlighted in a different color?

scott-fleischman

Lambda Calculus

Church, Alonzo. The Calculi of Lambda Conversion. Princeton University Press, 1941.

Barendregt, Henk P. The Lambda Calculus. North Holland, revised edition, 1984.

Barendregt, Henk P. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 7, pages 321–364. Elsevier / MIT Press, 1990.

Hindley, J. Roger and Jonathan P. Seldin. Introduction to Combinators andλ-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

scott-fleischman

module GreekScript3 where

data Empty : Set where

Not : Set → Set
Not x = x → Empty

data _And_ (A B : Set) : Set where
  _and_ : (a : A) → (b : B) → A And B

scott-fleischman

module ResolveMaybe where

data Maybe (A : Set) : Set where
  none : Maybe A
  some : A → Maybe A

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

scott-fleischman

using System;
using System.Collections.Generic;
using System.Linq;
using static System.Console;
using static System.Math;
using static Functional;

public static class Functional
{
	public static Func<X, Z> Compose<X, Y, Z>(Func<Y, Z> g, Func<X, Y> f) => x => g(f(x));

scott-fleischman

ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.2 for x86_64-apple-darwin):
	Simplifier ticks exhausted
  When trying UnfoldingDone $j_sdNBZ
  To increase the limit, use -fsimpl-tick-factor=N (default 100)
  If you need to do this, let GHC HQ know, and what factor you needed
  To see detailed counts use -ddump-simpl-stats
  Total ticks: 63261443

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

scott-fleischman

Writing Programs That Construct Proofs, Constable et al. 1984.
Beautiful introduction. Quite readable without much knowledge. Discusses λ-PRL. Defines tactics and tacticals.

Constructive Mathematics and Automatic Program Writers, Constable 1971

Lots of literature here