AndrasKovacs

{-# 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

{-# 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

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

-- Examples

data Foo = A | B | C

foo :: Foo -> Int
foo A = 10
foo B
foo C = 20

foo :: Foo -> Int

AndrasKovacs

{-
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

{-# 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

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

{-# 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

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

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 _$_ _$'_