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)

	// https://github.com/MaisaMilena/kaelin/blob/db1eff57aaca6d0936e1a9210da0855c5d17d45a/formality/stdlib/kaelin.fmc

	// ## Kaelin
	//
	// A simple, blockhain-enabled MOBA implemented in Formality-Core.
	//
	// Kaelin aims to capture some of the spirit of a MOBA, inluding map awareness,
	// micro and macro strategies, resource control, team-fights, skillshots and so
	// on, while aiming blockchain-compatible by being very lightweight (the entire
	// game state has only 8192 bits) and based on ~20 second turns. This allows it

	# ./HVM.hs #

	# HVM

	HVM is functional language and prover based on the Interaction Calculus.

	It is a pure functional runtime like Haskell's GHC, with some peculiarities:
	- Variables are affine, meaning they can only occur, at most, once.
	- To copy values, linear thunks are used, where 2 vars refer to the same value.
	- Accessing a thunk triggers an incremental, layer-by-layer copy of the value.

	#include <ctype.h>
	#include <stdbool.h>
	#include <stdint.h>
	#include <stdio.h>
	#include <stdlib.h>
	#include <string.h>

	typedef struct {
	const char* input;
	size_t index;

	-- TASK: create a Parser for Kind7.
	-- - don't be inventive, just use a simple approach that is guaranteed to work
	-- - keep it simple and idiomatic
	-- - include nice error messages

	-- On the 'parseApp parser:
	-- - support (f x y z) as an alias to (((f x) y) z)
	-- - do so by parsing '(', then terms until you hit a ')', then foldl to build the App

	-- Note on operators:

	# 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.