Skip to content

Instantly share code, notes, and snippets.

Avatar

András Kovács AndrasKovacs

View GitHub Profile
@AndrasKovacs
AndrasKovacs / HOASOnly.hs
Last active March 31, 2023 08:02
HOAS-only lambda calculus
View HOASOnly.hs
{-# 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 14, 2023 23:08
TT in TT using Prop + setoid fibrations
View TTinTTasSetoid.agda
{-# 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 February 18, 2023 12:08
Higher induction-induction-recursion
View HIIRT.md

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
View Or.txt
-- 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
View NbESharedQuote.hs
{-
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
View ImpredTmAlg.agda
{-# 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
@AndrasKovacs
AndrasKovacs / TypeDesc.v
Created January 8, 2022 14:00
Levitated type descriptions in Coq
View TypeDesc.v
Require Import Coq.Unicode.Utf8.
(*
As far as I can tell, there is way more literature in Agda on datatype-generic
programming than in Coq. I think part of the reason is that the Agda literature
makes liberal use of induction-recursion and fancy termination/positivity
checking, to define fixpoints of functors. These features are not available in
Coq.
@AndrasKovacs
AndrasKovacs / UnivPoly.hs
Last active November 6, 2022 18:56
Simple universe polymorphism with non-first-class levels
View UnivPoly.hs
{-# language LambdaCase, Strict, OverloadedStrings, DerivingVia #-}
{-# options_ghc -Wincomplete-patterns #-}
{-|
Simple universe polymorphism. Features:
- Non-first-class levels: there is a distinct Pi, lambda and application for
levels. Levels are distinct from terms in syntax/values.
- The surface language only allows abstraction over finite levels. Internally,
@AndrasKovacs
AndrasKovacs / GEqSpine.agda
Created October 20, 2021 08:31
Generic Eq for spine neutral inductive terms
View GEqSpine.agda
open import Relation.Binary.PropositionalEquality
renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
infixr 3 _⇒_
infix 3 sort⇒_
infixl 2 _▶_
infix 2 _$_
infixr 4 _∷_ _∷'_
@AndrasKovacs
AndrasKovacs / GEq.agda
Created October 19, 2021 22:14
Generic Eq for term algebras in Agda
View GEq.agda
open import Relation.Binary.PropositionalEquality
renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Function hiding (_$_)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
infixr 3 _⇒_
infix 3 sort⇒_
infixl 2 _▶_
infixl 2 _$_ _$'_