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
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.
| {-# language | |
| BlockArguments | |
| , CPP | |
| , LambdaCase | |
| , MagicHash | |
| , PatternSynonyms | |
| , Strict | |
| , TypeApplications |
| {-# 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 |
| {-# language | |
| BlockArguments | |
| , ConstraintKinds | |
| , ImplicitParams | |
| , LambdaCase | |
| , OverloadedStrings | |
| , PatternSynonyms | |
| , Strict | |
| , UnicodeSyntax | |
| #-} |
| {-# 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. |
| {-# 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 |
| {-# 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: |
| 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. |
| {-# LANGUAGE | |
| LambdaCase, GADTs, TypeOperators, TypeFamilies, DataKinds #-} | |
| data Type = TInt | TBool | Type :=> Type | |
| -- Needs GHC >= 7.8 | |
| type family Interp (t :: Type) where | |
| Interp TInt = Int | |
| Interp TBool = Bool | |
| Interp (a :=> b) = Interp a -> Interp b |