| // A nano dependent type-checker featuring inductive types via self encodings. | |
| // All computation rules are justified by interaction combinator semantics, | |
| // resulting in major simplifications and improvements over old Kind-Core. | |
| // Specifically, computable annotations (ANNs) and their counterpart (ANN | |
| // binders) and a new self encoding based on equality (rather than dependent | |
| // motives) greatly reduce code size. A more complete file, including | |
| // superpositions (for optimal unification) is available on the | |
| // Interaction-Type-Theory repository. | |
| // Credits also to Franchu and T6 for insights. |
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
| type t = Lexing.lexbuf -> Parser.token | |
| val of_file : string -> t * Lexing.lexbuf | |
| (** [of_file path] returns a new lexer for extracting tokens from | |
| a file at [path]. *) |
| type term = | |
| | Lam of (term -> term) | |
| | Pi of term * (term -> term) | |
| | Appl of term * term | |
| | Ann of term * term | |
| | FreeVar of int | |
| | Star | |
| | Box | |
| let unfurl lvl f = f (FreeVar lvl) |
| -- https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/extending_ghc.html#compiler-plugins | |
| -- https://downloads.haskell.org/~ghc/9.0.1/docs/html/libraries/ghc-9.0.1/GHC-Plugins.html | |
| module DerivingViaPlugin where | |
| import qualified Control.Monad as Monad | |
| import qualified GHC.Data.Bag as G | |
| import qualified GHC.Hs as G | |
| import qualified GHC.Plugins as P | |
| import qualified GHC.Types.Basic as G |
| ;;; Code: | |
| (global-set-key (kbd "M-g a") "α") | |
| (global-set-key (kbd "M-g b") "β") | |
| (global-set-key (kbd "M-g g") "γ") | |
| (global-set-key (kbd "M-g d") "δ") | |
| (global-set-key (kbd "M-g e") "ε") | |
| (global-set-key (kbd "M-g z") "ζ") | |
| (global-set-key (kbd "M-g h") "η") | |
| (global-set-key (kbd "M-g q") "θ") | |
| (global-set-key (kbd "M-g i") "ι") |
| {- cabal: | |
| build-depends: base, constraints | |
| -} | |
| {-# language TypeFamilies, TypeFamilyDependencies, ConstraintKinds, ScopedTypeVariables, NoStarIsType, TypeOperators, TypeApplications, GADTs, AllowAmbiguousTypes, FunctionalDependencies, UndecidableSuperClasses, UndecidableInstances, FlexibleInstances, QuantifiedConstraints, BlockArguments, RankNTypes, FlexibleContexts, StandaloneKindSignatures, DefaultSignatures #-} | |
| -- ⊷, ≕, =∘, =◯ These choices all look like something out of Star Trek, so let's boldly go... | |
| import Data.Constraint hiding (top, bottom, Bottom) | |
| import Data.Kind | |
| import Data.Some |
| module FoldsAndUnfolds where | |
| import Data.List -- for unfoldr | |
| class Functor f => Recursive f t | t -> f where | |
| project :: t -> f t | |
| cata :: (f a -> a) -> t -> a | |
| cata alg = go where go = alg . fmap go . project |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| module TLRecursionSchemes where | |
| import qualified GHC.TypeLits as TL |
| -- Solving Fix / Mu / Nu exercise in | |
| -- https://stackoverflow.com/questions/45580858/what-is-the-difference-between-fix-mu-and-nu-in-ed-kmetts-recursion-scheme-pac | |
| {-# LANGUAGE RankNTypes, GADTs #-} | |
| ---------------------------------------- | |
| -- Fix / Mu / Nu | |
| newtype Fix f = Fix { unFix :: f (Fix f) } |
