EduardoRFS

(* this whole thing is a sketch *)
type var = int [@@deriving show { with_path = false }]

type term =
  | T_var of var
  | T_let of var * term * term
  | T_lambda of var * term
  | T_apply of term * term
  | T_reify of thunk

EduardoRFS

module Syntax = struct
  type var = string

  type term =
    | T_var of var
    | T_let of var * term * term
    | T_annot of term * term
    | T_with_self of term * term
    (* pi *)
    | T_forall of var * term * term

EduardoRFS

Pi-Sigma-Self

The following is a set of syntax-directed rules to typing a dependently type system with self types. This is hopefully decidable given decidable conversion checking.

The main innovation is that all introduction rules propagate the self due to the new type of checking rule. This allows the fixpoint to be transparent to introductions, when combined with pairs, this leads to mutual recursion and the inductive types.

This doesn't define any universe or restriction to fixpoints, as those are more or less orthogonal to the typing issues here.

Syntax

riogu

using some templates with some hacky macros to allow matching on the contents of a std::variant, and getting the underlying value immediately.

also ignores if we match() on unique_ptr/shared_ptr/stack variable, match() works the same.

rntz

import bisect
from dataclasses import dataclass

class Bound:
    def to_bound(self): return self
    def __lt__(self, other):
        return self <= other and self != other
    def __le__(self, other):
        if isinstance(self, Init) or isinstance(other, Done): return True
        if isinstance(self, Done) or isinstance(other, Init): return False

rntz

-- A lower bound in a totally ordered key-space k; corresponds to some part of an
-- ordered sequence we can seek forward to.
data Bound k = Init | Atleast !k | Greater !k | Done deriving (Show, Eq)
instance Ord k => Ord (Bound k) where
  Init      <= _         = True
  _         <= Done      = True
  _         <= Init      = False
  Done      <= _         = False
  Atleast x <= Atleast y = x <= y
  Atleast x <= Greater y = x <= y

alt-romes

{- cabal:
build-depends: base, random, containers
-}
{-# LANGUAGE GADTs, ViewPatterns, GHC2021 #-}
import Text.Printf
import Control.Monad (liftM, ap)
import Data.Function (on)
import Data.List (sort, minimumBy)
import System.Random
import qualified Data.Map as M

roboguy13

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Relation.Nullary

module MonoidNat3 where

data Expr : Set where

Lysxia

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where

TOTBWF

(** {1 Syntax} *)

(** Expressions. *)
type expr =
  | Var of cont * int
  (** Local references.

      Thorin is a "blockless" IR, so we can reference arguments of
      other nodes by adding a data dependency edge, which implicitly
      nests the two nodes. *)