Skip to content

Instantly share code, notes, and snippets.

Avatar

AndrasKovacs

View GitHub Profile
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
@AndrasKovacs
AndrasKovacs / MonadicNbE.hs
Last active Feb 28, 2021
Notes on normalization-by-evaluation modulo monad laws for monadic language
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
@AndrasKovacs
AndrasKovacs / cont-cwf.agda
Created Jun 18, 2020 — forked from bobatkey/cont-cwf.agda
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
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)
@AndrasKovacs
AndrasKovacs / GluedEval.hs
Last active Dec 29, 2020
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
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
@AndrasKovacs
AndrasKovacs / FixNf.hs
Last active Jan 26, 2021
Minimal environment machine normalization with a fixpoint operator
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