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

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

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

English Corpora

BYU Law & Corpus Linguistics

https://lawncl.byu.edu/

The Oxford English Corpus (OEC)

Corpus of Contemporary American English (COCA)

https://corpus.byu.edu/coca/

scott-fleischman

-- taken from http://stackoverflow.com/questions/21349408/zip-with-default-value-instead-of-dropping-values/21350096#21350096

module Main where

import Control.Applicative
import Data.Traversable
import Data.List

data Padme m = (:-)
  { padded :: [m]

scott-fleischman

module AgdaGreek4 where

open import Data.Maybe renaming (nothing to ⃠)
open import Data.Vec
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≢_)

data Case : Set where
  lower upper : Case

scott-fleischman

-- See "The Zipper" by Huet 1997

module Main where

import Control.Applicative
import Control.Monad
import Data.Either

data Tree a =
    Item a

scott-fleischman

module Main where

primes = 2 : [x | x <- [3..], isprime x]
isprime x = all (\p -> x `mod` p > 0) (factorsToTry x)
  where
    factorsToTry x = takeWhile (\p -> p*p <= x) primes

main = do
  let ps = take 10000 primes
  putStrLn $ (show . length $ ps) ++ " primes."

scott-fleischman

Thoughts on Citations on Twitter

I often post quotes on Twitter without citing the source. I have a few
reasons for doing that. 

First, Twitter is a limited medium for expression, and as such, I
usually find that the quote I want to tweet does not fit within 140
characters. Limiting the expression even more by including a citation
is too burdensome. Likewise, I don't want to reply to every one of my
tweets with the citation—that would be too many tweets. It's

scott-fleischman

-- http://www.seas.upenn.edu/~cis194/hw/12-monads.pdf
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Risk where

import Control.Monad
import Control.Monad.Random
import Control.Applicative
import Data.List
import Data.Monoid