Hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

Hirrolot

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

xarvh

#!/usr/bin/env node

// A work around to https://github.com/avh4/elm-format/issues/352

// * Use it in place of elm-format (only some flags are supported)
// * Run it from a directory containing node_modules/elm-format/bin/elm-format (but you can change it below)


function extractFirstRegexMatch(regex, elmCode) {

pesterev

type CamelCaseKeys<T extends unknown> = {
   [K in keyof T as CamelCaseKey<K>]: T[K]
}

type CamelCaseKey<T> = T extends `${infer T0}_${infer T1}` ? `${T0}${CamelCaseKeyN<T1>}` : T

type CamelCaseKeyN<T> = T extends `${infer T0}_${infer T1}` ? `${Sentence<T0>}${CamelCaseKeyN<T1>}` : Sentence<T>

type Sentence<T> = T extends `${infer T0}${infer T1}` ? `${Uppercase<T0>}${T1}` : T

pesterev

type UniqueParser0<T, R extends unknown[], M> = Readonly<T> extends readonly [] ? T : UniqueParser1<T, R, M>

type UniqueParser1<T, R extends unknown[], M> = Readonly<T> extends readonly [infer _] ? T : UniqueParserN<T, R, M>

type UniqueParserN<T, R extends unknown[], M> = Readonly<T> extends readonly [infer A, ...infer B] ? A extends M ? UniqueParserTerm<B, R, M> : UniqueParserTerm<B, [...R, A], M | A>  : never

type UniqueParserTerm<T, R extends unknown[], M> = Readonly<T> extends readonly [] ? R : UniqueParserN<T, R, M>

export type UniqueTuple<T> = UniqueParser0<T, [], never>

AndrasKovacs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val

AndrasKovacs

{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,
             TypeInType, StandaloneDeriving #-}

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

codedot

all:
	node work2mlc.js getwork.json 381353fa >test.mlc
	lambda -pem lib.mlc -f test.mlc

clean:

camsaul

;;; -*- tab-width: 2 -*-

;;; These four lines go at the beginning of almost every code file. 16-byte iNES header

  .inesprg 1                      ; one bank of program code
  .ineschr 1                      ; one bank of picture data
  .inesmap 0                      ; we use mapper 0
  .inesmir 1                      ; Mirror setting always 1

;;; BANKING