atennapel

module Self where

-- core language
type Ix = Int

data Core
  = Var Ix
  | Abs Core
  | App Core Core
  | Pi Core Core

atennapel

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

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');