Skip to content

Instantly share code, notes, and snippets.

View AndrasKovacs's full-sized avatar

András Kovács AndrasKovacs

View GitHub Profile
@AndrasKovacs
AndrasKovacs / GluedEval.hs
Last active January 20, 2025 21:55
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
{-# 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 May 30, 2025 12:53
Minimal environment machine normalization with a fixpoint operator
{-# 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
@AndrasKovacs
AndrasKovacs / CCCNbE.agda
Last active March 17, 2021 18:11
NbE for CCC
open import Data.Unit
open import Data.Product
infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_
data Obj : Set where
∙ : Obj
base : Obj
_*_ : Obj → Obj → Obj
@AndrasKovacs
AndrasKovacs / CellularUnrolled.hs
Created December 11, 2019 23:14
cellular automata
{-# 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
@AndrasKovacs
AndrasKovacs / Cellular.hs
Last active April 10, 2020 07:29
Cellular automata
{-# language Strict #-}
import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word
type Rule = A.PrimArray Word8
mkRule :: Word8 -> Rule
@AndrasKovacs
AndrasKovacs / Ordinals.agda
Last active June 16, 2025 15:19
Large countable ordinals and numbers in Agda
{-# OPTIONS --postfix-projections --without-K --safe #-}
{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.
Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:
@AndrasKovacs
AndrasKovacs / IITfromNat.agda
Last active May 14, 2020 00:22
Constructing finitary inductive types from natural numbers
{-# OPTIONS --without-K #-}
{-
Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
quotients. Sketch in two parts.
1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
Here I only show this for really simple, single-sorted closed inductive types,
but it should work for indexed inductive types as well.
@AndrasKovacs
AndrasKovacs / CumulativeIRUniv.agda
Last active October 6, 2020 12:09
Transfinite, cumulative, Russell-style, inductive-recursive universes in Agda.
{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.
Checked with: Agda 2.6.1, stdlib 1.3
My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:
@AndrasKovacs
AndrasKovacs / SysF.hs
Created December 1, 2018 12:19
intrinsic deep system F syntax in Haskell
{-# language
TypeInType, GADTs, RankNTypes, TypeFamilies,
TypeOperators, TypeApplications,
UnicodeSyntax, UndecidableInstances
#-}
import Data.Kind
import Data.Proxy
data Nat = Z | S Nat
@AndrasKovacs
AndrasKovacs / FunListPerm.hs
Last active November 7, 2018 16:50
Funlist permutations challenge
{-# language GADTs #-}
-- https://www.reddit.com/r/haskell/comments/9uz2f5/code_challenge_welltyped_tree_node_order/
data Tree a where
OneT :: a -> Tree a
Ap :: (a -> b -> c) -> Tree a -> Tree b -> Tree c
data FunList a where