Skip to content

Instantly share code, notes, and snippets.

View rybla's full-sized avatar

Henry Blanchette rybla

View GitHub Profile
@rybla
rybla / Transpose.agda
Last active August 4, 2022 21:30
transpose and identity of vector-matrices in Agda
open import Data.Nat
data Vec : ℕ → Set → Set where
nil : ∀ {A} → Vec 0 A
cons : ∀ {A n} → A → Vec n A → Vec (suc n) A
record Traversable (F : Set → Set) : Set1 where
field
traverse : ∀ {S T : Set} {G : Set → Set} → (S → G T) → F S → G (F T)
@rybla
rybla / GenericPath.purs
Created December 19, 2022 19:11
Generic Paths in Purescript
--------------------------------------------------------------------------------
-- Tree
--------------------------------------------------------------------------------
data Tree a
= Tree a (Array (Tree a))
instance functorTree :: Functor Tree where
map f (Tree a ts) = Tree (f a) (map f <$> ts)
instance applyTree :: Apply Tree where

(based on a conversation I had with Jacob Prinz)

SYSTEM

You are a knowledgeable programming languages assistant. You help the user analyze a new programming language.

USER

Slrj is a new programming language. The grammar of Slrj expressions is defined as follows, where "x" is any Slrj expression, and "A", "B", and "C" are atomic values.

@rybla
rybla / chat1.md
Last active March 6, 2024 00:12
Aljc.chat.md

Based on Slrj.chat.md; inspired by a conversation with aljce

User

You are a knowledgeable programming languages assistant. You help the user analyze a new programming language.

Aljc is a new programming language. The grammar of Aljc expressions is defined as follows, where x is any Aljc expression and A, B, and C are atomic values.

x ::= A | B | C | (x x)
@rybla
rybla / MyExistsConstrained.purs
Last active April 24, 2025 14:57
Pattern for existential types with typeclass constraints
module Data.MyExistsConstrained where
import Prelude
import Unsafe.Coerce (unsafeCoerce)
-- Suppose you want to use an existentially-quantified type. You can use the
-- `exists` package, which defines `Exists` likes so:
foreign import data Exists :: (Type -> Type) -> Type
@rybla
rybla / polymorphic_records_and_variants.ts
Last active July 12, 2024 19:59
in typescript, polymorphic records and variants
/*
The idea of this implementation is that a row (`Row`) serves as the
specification of either:
- a record (`Record<T extends Row>`) which is an object that, for each of the
elements of the row, has a key-value mapping from the element's tag to the
element's domain
- a variant (`Variant<T extends Row>`) which is a union of the row elements.
*/
type Tuple = any[]
@rybla
rybla / IntrinsicSimpleLambdaCalculus.purs
Created July 26, 2024 14:35
intrinsically-typed simply-typed lambda calculus in Purescript
module Languages.IntrinsicallyTypedLambdaCalculus where
import Prelude hiding (($), type (~>))
import Data.Symbol (class IsSymbol)
import Prim.Row (class Cons)
import Type.Proxy (Proxy(..))
-- =============================================================================
// while iterating, have a `mut bindings: Vec<Bindings>`
// have a structure of Scopes that contain references to values in `bindings`
// a Binding doesn't refer to a Scope
// at the end, return `bindings`, so Scopes cannot own anything in bindings
// mutable reference is a subtype of immutable reference
fn example<'source>(
bindings: &mut Vec<Box<Binding<'source>>>,
names: Vec<&'source str>,
) {
@rybla
rybla / Main.purs
Created August 10, 2024 01:58
example Halogen app setup
module Main where
import Prelude
import Effect (Effect)
import Effect.Aff.Class (class MonadAff)
import Halogen as H
import Halogen.Aff as HA
import Halogen.HTML as HH
import Halogen.VDom.Driver as HVD
@rybla
rybla / Main.purs
Created September 21, 2024 16:14
simple http server in Purescript
import Prelude
import Effect (Effect)
import Effect.Aff (launchAff_)
import Effect.Class (liftEffect)
import Effect.Class.Console as Console
import Node.Encoding (Encoding(..))
import Node.EventEmitter (on_, once_)
import Node.FS.Sync as FS
import Node.HTTP (createServer)