mb64

kind ty type.

type tunit  ty.
type tfun   ty -> ty -> ty.
type tall   (ty -> ty) -> ty.

kind tm type.

type unit   tm.
type app    tm -> tm -> tm.

mb64

(* Compile with:
  $ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
Example use:
  $ ./tychk <<EOF
  > let f = (fun x -> x) : forall a. a -> a
  > in f f
  > EOF
  input : forall a. a -> a
*)

mb64

#!/bin/bash

# Source: https://taylor.fausak.me/2021/11/16/haskell-survey-results
wget https://taylor.fausak.me/static/pages/2021-state-of-haskell-survey-results.json.zip
unzip 2021-state-of-haskell-survey-results.json.zip

echo "Question: If you wanted to convince someone to use Haskell, what would you say?" > q1-convince.txt
echo "---" >> q1-convince.txt
jq -r 'map(.s9q0 | .[]?) | join("\n---\n")' < 2021-state-of-haskell-survey-results.json >> q1-convince.txt

mb64

-- Normalization by Evaluation for STLC, in Agda
--
-- Partially based on "NbE for CBPV and polarized lambda calculus" (Abel, 2019)

open import Function

infixr 5 _⇒_
infixl 4 _,_
infix 2 _⊃_

mb64

type name = string

module AST = struct
  type ty =
    | TFun of ty * ty
    | TNamed of string
    | TApp of ty * ty

  type exp =
    | Annot of exp * ty

mb64

(* Typechecker for MLTT with a universe hierarchy *)
(* Build with: ocamlfind ocamlc -package angstrom,stdio -linkpkg mltt.ml -o mltt *)
type name = string

module AST = struct
  type tm =
    | Var of name
    | U of int
    | Pi of name * ty * ty
    | Annot of tm * ty

mb64

(* Itty bitty SMT solver: DPLL(T) where T = equality *)
(*
# let x, y = 0, 1 (* integer variable IDs *) ;;
# let prob = SMT.new_problem 2 (* 2 for two variables *) ;;
# let b = SMT.new_bool prob;;  
# SMT.add_clause prob [b; SMT.eq prob x y];
  SMT.add_clause prob [SMT.not b];
  SMT.solve prob;;
- : SMT.response = SMT.SAT
# SMT.add_clause prob [SMT.not (SMT.eq prob x y)];