View Universes.agda
{-# OPTIONS --postfix-projections --without-K #-} | |
-- Notes for https://www.youtube.com/watch?v=RXKRepPm0ps | |
-- checked with Agda 2.6.1 + stdlib 1.5 | |
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂) | |
open import Relation.Binary.PropositionalEquality | |
renaming (subst to tr; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; cong to ap) | |
open import Data.Nat |
View MonadicNbE.hs
{- | |
-- Compiler: staging, memory layout control, etc (small + self-hosting + useful soon) | |
-- Surface language: | |
1. CBV + side effects (ML) | |
2. CBV + typed effect system: | |
- Eff monad | |
- Eff monad, row of effects | |
f : Int -> Eff [IO, Exc e, MutRef a, MutRef b] Int |
View TransformTyped.hs
-- solution to https://github.com/effectfully/haskell-challenges/blob/master/h3-transform-typed/README.md | |
{-# LANGUAGE GADTs #-} | |
module Lib where | |
import Data.Proxy | |
import Data.Typeable | |
data Scheme a where |
View ForceElems.hs
-- Solution to challenge: https://github.com/effectfully/haskell-challenges/tree/master/force-elems | |
-- (Spoiler) | |
data EC = Elem | Con | |
data T a = T {ec :: !EC, unT :: a} | |
appEC :: EC -> (a -> b) -> a -> b | |
appEC Elem f a = f $! a | |
appEC Con f a = f a |
View Cantor.agda
{-# OPTIONS --without-K #-} | |
open import Data.Bool | |
open import Data.Product | |
open import Relation.Binary.PropositionalEquality | |
open import Data.Empty | |
open import Function | |
surj : {A B : Set} → (A → B) → Set | |
surj f = ∀ b → ∃ λ a → f a ≡ b |
View cont-cwf.agda
{-# OPTIONS --rewriting #-} | |
module cont-cwf where | |
open import Agda.Builtin.Sigma | |
open import Agda.Builtin.Unit | |
open import Agda.Builtin.Bool | |
open import Agda.Builtin.Nat | |
open import Data.Empty | |
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; trans; subst; cong) |
View GluedEval.hs
{-# language Strict, LambdaCase, BlockArguments #-} | |
{-# options_ghc -Wincomplete-patterns #-} | |
{- | |
Minimal demo of "glued" evaluation in the style of Olle Fredriksson: | |
https://github.com/ollef/sixty | |
The main idea is that during elaboration, we need different evaluation |
View FixNf.hs
{-# language Strict, BangPatterns #-} | |
data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq) | |
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm | |
isCanonical :: Val -> Bool | |
isCanonical VLam{} = True | |
isCanonical _ = False | |
eval :: [Val] -> Tm -> Val |
View CCCNbE.agda
open import Data.Unit | |
open import Data.Product | |
infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_ | |
data Obj : Set where | |
∙ : Obj | |
base : Obj | |
_*_ : Obj → Obj → Obj |
View CellularUnrolled.hs
{-# language Strict, TypeApplications, ScopedTypeVariables, | |
PartialTypeSignatures, ViewPatterns #-} | |
{-# options_ghc -Wno-partial-type-signatures #-} | |
import qualified Data.Primitive.PrimArray as A | |
import GHC.Exts (IsList(..)) | |
import Data.Bits | |
import Data.Word | |
import Control.Monad.ST.Strict |
NewerOlder