Skip to content

Instantly share code, notes, and snippets.

View atennapel's full-sized avatar

Albert ten Napel atennapel

39 followers · 31 following
  • Netherlands
View GitHub Profile
@atennapel
atennapel / RTValidation.ts
Last active August 23, 2019 15:16
Runtime type validation in TypeScript
type Validator<T> = (val: any) => T | Error;
type ValidatorExtract<V> = V extends Validator<infer T> ? T : never;
type ValidatorMap = { [key: string]: Validator<any> };
const err = (ty: string) => new Error('validate failed: ' + ty);
const nullV: Validator<null> = (val: any) =>
val === null ? val : err('null');
const undefinedV: Validator<undefined> = (val: any) =>
typeof val === 'undefined' ? val : err('undefined');
@atennapel
atennapel / CC.hs
Last active July 4, 2020 06:17
Calculus of Constructions, normalization-by-evaluation, semantic typechecking
data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Fix Tm | Uni
data Clos = Clos Tm Env
data Dm = DVar Int | DAbs Clos | DNeutral Int [Dm] | DPi Dm Clos | DFix Clos | DUni
type Env = [Dm]
capp :: Clos -> Dm -> Dm
capp (Clos b e) t = eval (t : e) b
vapp :: Dm -> Dm -> Dm
vapp a b =
@atennapel
atennapel / Self.hs
Created May 30, 2021 14:45
Self types
module Self where
-- core language
type Ix = Int
data Core
= Var Ix
| Abs Core
| App Core Core
| Pi Core Core
@atennapel
atennapel / UnivPoly.hs
Last active July 7, 2021 04:51
Universe Polymorphism
-- universe polymorphism
module UnivPoly where
-- core language
type Ix = Int
data Term
= Var Ix
| Abs Term
| App Term Term
@atennapel
atennapel / finitary.agda
Last active January 4, 2022 17:50
Finitary non-indexed datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
PiInd : Ty -> Ty
@atennapel
atennapel / infinitary.agda
Created January 4, 2022 14:23
Infinitary non-indexed datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ind : Set where
U : Ind
Pi : (A : Set) -> (A -> Ind) -> Ind
@atennapel
atennapel / finite.agda
Created January 4, 2022 14:25
Finite datatypes signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
record Ty : Set where
instance constructor U
data Ctx : Set where
@atennapel
atennapel / non-inductive.agda
Created January 4, 2022 14:26
Non-inductive datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
@atennapel
atennapel / infinitary-indexed-uncurried.agda
Created January 4, 2022 15:39
Infinitary indexed datatypes signatures with uncurried index
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ix : Set where
U : Ix
Pi : (A : Set) -> (A -> Ix) -> Ix
@atennapel
atennapel / infinitary-indexed-single-index.agda
Last active January 5, 2022 14:34
Infinitary indexed datatype signatures with a single index
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Data.Product
data Ind (I : Set) : Set where
U : I -> Ind I
Pi : (A : Set) -> (A -> Ind I) -> Ind I