Skip to content

Instantly share code, notes, and snippets.

@rntz
rntz / not-actually-agda.agda
Last active March 18, 2024 12:07
fake agda for preorder theory
record Preorder (A : Set) : Set1 where
_≤_ : A A Set
refl : {a} a ≤ a
trans : {a b c} a ≤ b b ≤ c a ≤ c
record is-lub {A} (P : Preorder A) {I} (a : I A) (⋁a : A) : Set where
bound : (i : I) a i ≤ ⋁a
least : (b : A) ((i : I) a i ≤ b) ⋁a ≤ b
module _ {A B} (P : Preorder A) (Q : Preorder B) (f : A B) where
/* Examples of ways in which 'void' is not a unit type in C: */
void baz(void p) { /* error: argument may not have 'void' type */
return p; /* error: void function 'baz' should not return a value [-Wreturn-type] */
}
struct foo {
void field; /* error: field has incomplete type 'void' */
};
data Regex = Class [Char] -- character class
| Seq [Regex] -- sequence, ABC
| Choice [Regex] -- choice, A|B|C
| Star Regex -- zero or more, A*
deriving (Show)
-- The language of a regex is, in theory, defined inductively as follows, substituting
-- lists for mathematical sets.
naive :: Regex -> [String]
naive (Class chars) = [[c] | c <- chars]
@rntz
rntz / regex-size.hs
Last active September 12, 2023 00:30
-- THIS CODE IS COMPLETELY WRONG
import qualified Data.List as List
data Regex = Class [Char] -- character class
| Seq [Regex] -- sequence, ABC
| Choice [Regex] -- choice, A|B|C
| Star Regex -- zero or more, A*
deriving (Show)
{-# LANGUAGE GADTs, TypeFamilies #-}
data Type a where
TNat :: Type Int
TFun :: Type a -> Type b -> Type (a -> b)
type Var a = (Type a, String)
data Expr a where
ENat :: Int -> Expr Int
EVar :: Var a -> Expr a
ELam :: Var a -> Expr b -> Expr (a -> b)

We want to maintain the sequence of iterations of some function f,

f: I × S → S

I: “input” from external world - list of edges, for example S: “state” of iteration, needs an initial value - a frontier, for example

iterate : I × S → Stream S iterate (input, state) = state :: iterate (input, f (input, state))

chart
(A,A') -> (B,B')
lens
get : A -> B
put : A × B' -> A'
chart
get : A -> B
weird : A × A' -> B'
import Data.List
interface Cat obj (0 hom: obj -> obj -> Type) where
id : {a: obj} -> hom a a
seq: {a, b, c: obj} -> hom a b -> hom b c -> hom a c
interface Cat (List obj) hom => Concat obj hom where
para: {Γ₁, Γ₂, Δ₁, Δ₂ : List obj}
-> hom Γ₁ Δ₁ -> hom Γ₂ Δ₂
-> hom (Γ₁ ++ Γ₂) (Δ₁ ++ Δ₂)
from talon import Module, Context, actions
from typing import Any, NamedTuple, Union, Optional
from dataclasses import dataclass
import logging
mod = Module()
ctx = Context()
# Types.
Motion = Union[str, tuple]