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)
| ╭──────────────────────────────────────────────────────────────╮ | |
| │ ● 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 |
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]
| import Control.Monad (when) | |
| import Data.Char (chr, ord) | |
| import Data.IORef | |
| import Data.Word | |
| import Debug.Trace | |
| import System.IO.Unsafe (unsafePerformIO) | |
| import Text.Parsec hiding (State) | |
| import qualified Data.IntMap.Strict as IntMap | |
| import qualified Data.Map as Map | |
| import qualified Text.Parsec as Parsec |