Victor Taelin VictorTaelin

I'm thinking on how to add funext to a Type Theory in the spirit of that answer

my understanding is that OTT, as presented, introduces computation rules for a built-in identity / propositional equality type. for example, in OTT, we'd have something like:

Eq (A,B) (a0,b0) (a1,b1)

reduce to

(Eq A a0 a1 , Eq B b0 b1)

Suppose you wanted to represent an 1D space in a pure functional language, i.e., with trees. Suppose that you also needed to shift the whole space left and right. An efficient way to do it would be to use a perfect binary tree to store locations, and bit-strings to represent paths. For example:

(((0 1) (2 3)) ((4 5) (6 7)))

The tree above would represent a space with 8 locations. Then, the path:

[1,0,0]

	# Bend prelude
	# ------------

	type Maybe<A: Set>:
	case @None:
	case @Some:
	value: A

	type Result<F: Set, D: Set>:
	case @Done:

	╭──────────────────────────────────────────────────────────────╮
	│ ● OpenAI Codex (research preview) v0.1.2505172129 │
	╰──────────────────────────────────────────────────────────────╯
	╭──────────────────────────────────────────────────────────────╮
	│ localhost session: b966636e1ecf42a59c8fef1192074e17 │
	│ ↳ workdir: ~/vic/dev/bend │
	│ ↳ model: o3 │
	│ ↳ provider: openai │
	│ ↳ approval: suggest │
	╰──────────────────────────────────────────────────────────────╯

	module Main where

	import Data.List (nub)

	-- Pattern Matching Flattener Algorithm
	-- ====================================
	--
	-- This algorithm converts pattern matching expressions with multiple
	-- scrutinees into nested case trees with single scrutinees.
	--

	-- OldCheck:
	-- (omitted)

	# The Interaction Calculus

	The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
	is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
	with some key differences:
	1. Vars are affine: they can only occur up to one time.
	2. Vars are global: they can occur anywhere in the program.

	-- OldCheck:
	-- (omitted)

	# The Interaction Calculus

	The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
	is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
	with some key differences:
	1. Vars are affine: they can only occur up to one time.
	2. Vars are global: they can occur anywhere in the program.

	data Uni : Set where
	U : Uni

	data ℕ : Set where
	Z : ℕ
	S : ℕ → ℕ

	data Vec (A : Set) : ℕ → Set where
	[] : ∀{n} → Vec A n
	_::_ : ∀{n} → A → Vec A n → Vec A (S n)

	-- Let's serialize lists of uints as follows:
	--
	-- <Uint> ::= 0 \| 1 <Uint>
	-- <List> ::= 0 \| 1 <Uint> <List>
	--
	-- For example, [1,2,3] serializes to '1 10 1 110 1 1110 0'.
	--
	-- Let f be a function that, given a number N, and a list of
	-- numbers XS, sets the Nth number on XS to 0. For example:
	-- - f(2, [0,1,2,3,4]) = [0,1,0,3,4]

	import Prelude.hvml

	// Types
	// -----

	// Type ::= ⊥ \| [Type]
	// - ⊥ = ⊥ = the Empty type
	// - [⊥] = ⊤ = the Unit type
	// - [[⊥]] = ℕ = the Nat type
	// - [[[⊥]]] = ℕ* = the List type