Skip to content

Instantly share code, notes, and snippets.

@aradarbel10
aradarbel10 / Main.hs
Last active June 14, 2023 20:52
Type directed program synthesis for STLC
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use list comprehension" #-}
import Data.IORef ( IORef, newIORef, readIORef, writeIORef )
import GHC.IO ( unsafePerformIO )
import Control.Applicative ( Alternative(..) )
import Control.Monad ( when )
import Debug.Trace
@aradarbel10
aradarbel10 / natcomp.lagda.md
Last active June 14, 2023 20:28
A tiny formally-verified compiler from arithmetic expressions to a stack machine
module natcomp where

open import Data.Nat using (ℕ; _+_)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Properties using (++-assoc)
open import Data.Maybe using (Maybe; just; nothing; _>>=_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning
@aradarbel10
aradarbel10 / main.ml
Last active July 3, 2023 15:12
minimal STLC type inference with mutable metavars
(* language definition *)
type nom = string
type bop = Add | Sub | Mul
type typ =
| Int | Arrow of typ * typ | Meta of meta
and meta = meta_state ref
and meta_state =
| Solved of typ
| Unsolved of nom (* keep name for pretty printing *)
@aradarbel10
aradarbel10 / Main.hs
Created December 6, 2022 15:40
A minimalistic example of bidirectional type checking for system F
{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}
{-
(compiled with GHC 9.4.2)
-}
{-
HEADS UP
this is an example implementation of a non-trivial type system using bidirectional type checking.
it is...
@aradarbel10
aradarbel10 / contexts.lagda.md
Last active September 19, 2022 02:41
Category of contexts and context-renamings
{-# OPTIONS --without-K #-}

open import foundation.functions using (_∘_)
open import foundation.identity-types using (refl; ap) renaming (Id to _≡_)

Contexts

We think of contexts as snoc lists of types

@aradarbel10
aradarbel10 / parser_simple.mly
Last active September 6, 2022 22:00
Menhir (LR) grammar for pi types with syntactic sugar `(x y z : a) -> b` and `a -> b`
%{
(** the [Surface] module contains our AST. *)
open Surface
(** exception raised when a [nonempty_list] returns an empty list. *)
exception EmptyUnfolding
(** desugars `(x y z : a) -> b` into `(x : a) -> (y : a) -> (z : a) -> b`. *)
let rec unfoldPi (xs : string list) (dom : expr) (cod : expr) : expr =
match xs with
@aradarbel10
aradarbel10 / groupoid.agda
Created July 13, 2022 09:11
Direct proof for groupoidal structure of homotopic identity types via path induction in Agda
{-# OPTIONS --without-K #-}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
pattern erefl x = refl {x = x}
--- path induction ---
J : {A : Set} →