brendanzab

Weird field/param language

Further messing around on top of some ideas in the previous gist.

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

Grammar

term, type ::=\

brendanzab

Weird field/param language 2

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

This is a more succinct syntax than the previous gist, this time using in and out in place of param and record, and making introductions and eliminations more succinct.

Grammar

brendanzab

Weird binder language thingy

Playing around with a uniform notation for binders (eg. Π, Σ, λ, let). This is probably not the greatest language to program in directly, but I think it's fun to see if a more consistent syntax can help to expose some of the differences between dependent functions, dependent pairs, and let expressions...

Syntax

brendanzab

Quantifiers

Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.

Examples

{
 out id : {

brendanzab

Notation	Meaning
l ? T	abstract node in T
l : T	concrete node in T
l = t	node equal to t
default = t	reduce to this node if all nodes are concrete
{ ... }	graph term
t1.{ l = t2 }	updates node l in t1 to be t2
t.l	gets the value of node l in t
t.{ l1 -> l2 }	renames l1 to l2 in t

brendanzab

Combining Pi and Sigma types?

-- id : forall a. a -> a
-- id x = x

id : type [
    in A : Type, 
    in a : A, 
    out a' : A,

brendanzab

A graph-based core for a dependently typed language

Abstract

An overly-ambitious attempt to re-think the core calculus of dependent type theory by basing it on graphs as opposed to lambdas, Π-types, Σ-types, etc. The hope is that this might allow us to investigate dependency more closely, and allow us to refine programs to target different environments in an easier way than with traditional programming representations.

Introduction

brendanzab

{
  "record.term": {
    "fields": {
      "identity": { "node": "$identity" },
      "compose": { "node": "$compose" },
      "Unit": { "node": "$Unit" },
      "Bool": { "node": "$Bool" },
      "Option": { "node": "$Option" }
    },
    "nodes": {

brendanzab

# Concrete syntax:
#
# ```
# let
#   pi
#     : float/64
#     = 3.1415
#   identity ||< The polymorphic identity function
#     : [ A : Type  ||< The input type.
#       , a : A     ||< The input.

brendanzab

Weird type theory diagrams

I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these :sparkles: very informal :sparkles: Venn diagram thingies.

Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!

Syntax