Skip to content

Instantly share code, notes, and snippets.

View LightAndLight's full-sized avatar
🤓

Isaac Elliott LightAndLight

🤓
190 followers · 30 following
View GitHub Profile
@LightAndLight
LightAndLight / Reactive.hs
Last active March 1, 2020 06:36
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Reactive.hs
Created February 29, 2020 11:38
Patterns for building fine-grained reactive datatypes
data Triple f a b c
= Triple1 (f a) (f b) (f c)
| Triple2 (f a) (f b) (f c)
data TripleAction a b c where
Triple1Fst :: (a -> a) -> TripleAction a b c
Triple1Snd :: (b -> b) -> TripleAction a b c
Triple1Thd :: (c -> c) -> TripleAction a b c
@LightAndLight
LightAndLight / Irrel.agda
Last active February 18, 2020 01:46
Using irrelevance to get decent code extraction
module Irrel where
open import Data.Bool using (if_then_else_)
open import Data.Maybe using (Maybe; just; nothing; map; _>>=_)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (Σ; _,_)
open import Data.String using (String; _==_)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
@LightAndLight
LightAndLight / zippery typeclass elaboration
Created February 10, 2020 23:22
typeclasses in typechecking-in-context style?
x : ∀α₀, α₁, …, αₘ. (C₀, C₁, …, Cₙ) ⇒ τ
————–—————————————————————————————–————————————————————————————————————————————————————————————————————————————————–
(Θ ↓ x) ↦ (Θ, α₀ : *, α₁ : *, …, αₘ : *, ev₀ : C₀, ev₁ : C₁, …, evₙ : Cₙ ↑ x α₀ α₁ … αₘ ev₀ ev₁ … evₙ : τ)
—————————————————————————————————————————————————–
(Θ ↓ let x = v in e) ↦ (Θ, [let x = ⋄ in e] ↓ v)
solveConstraints(θ, Ξ) ↦ Ξ' gen(Ξ', τ) ↦ σ
—————————————————————————————————————————————————————————————
(Θ, [let x = ⋄ in e], Ξ ↑ v : τ) ↦ (θ, [let x : σ = v in ⋄] ↓ e)