Navigation Menu

Skip to content

Instantly share code, notes, and snippets.

View AndrasKovacs's full-sized avatar

András Kovács AndrasKovacs

View GitHub Profile
{-# language
BlockArguments
, CPP
, LambdaCase
, MagicHash
, PatternSynonyms
, Strict
, TypeApplications
@AndrasKovacs
AndrasKovacs / SetoidTTinTT.agda
Last active January 10, 2024 13:59
TT in TT using only induction-induction
{-# OPTIONS --without-K #-}
-- version 1, conversion is indexed over conversion
module IndexedConv where
data Con : Set
data Ty : Con → Set
data Sub : Con → Con → Set
data Tm : ∀ Γ → Ty Γ → Set
data Con~ : Con → Con → Set
{-# language
BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}
@AndrasKovacs
AndrasKovacs / ZeroCostGC.md
Last active April 6, 2024 17:07
Garbage collection with zero-cost at non-GC time

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

@AndrasKovacs
AndrasKovacs / HOASOnly.hs
Last active February 27, 2024 15:50
HOAS-only lambda calculus
{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}
{-|
Minimal dependent lambda caluclus with:
- HOAS-only representation
- Lossless printing
- Bidirectional checking
- Efficient evaluation & conversion checking
Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196
@AndrasKovacs
AndrasKovacs / TTinTTasSetoid.agda
Last active January 11, 2024 10:08
TT in TT using Prop + setoid fibrations
{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}
{-
Challenge:
- Define a deeply embedded faithfully represented syntax of a dependently typed
TT in Agda.
- Use an Agda fragment which has canonicity. This means that the combination of
indexed inductive types & cubical equality is not allowed!
- Prove consistency.
@AndrasKovacs
AndrasKovacs / HIIRT.md
Last active March 25, 2024 08:20
Higher induction-induction-recursion

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

@AndrasKovacs
AndrasKovacs / Or.txt
Last active December 1, 2022 07:20
Syntax proposal for or-patterns in Haskell
-- Examples
data Foo = A | B | C
foo :: Foo -> Int
foo A = 10
foo B
foo C = 20
foo :: Foo -> Int
@AndrasKovacs
AndrasKovacs / NbESharedQuote.hs
Last active May 2, 2023 01:02
NbE with implicit sharing in quotation
{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:
"A simple and efficient implementation of strong call by need by an abstract machine"
https://dl.acm.org/doi/10.1145/3549822
This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.
@AndrasKovacs
AndrasKovacs / ImpredTmAlg.agda
Last active June 29, 2022 14:23
Impredicative encodings as term algebra constructions
{-# OPTIONS --type-in-type #-}
open import Relation.Binary.PropositionalEquality
renaming (cong to ap; sym to infixl 6 _⁻¹; subst to tr; trans to infixr 4 _◾_)
open import Data.Product
renaming (proj₁ to ₁; proj₂ to ₂)
--------------------------------------------------------------------------------
NatAlg : Set