{{ message }}

Instantly share code, notes, and snippets.

# brendanzab/weird-core-language.md

Last active Aug 12, 2020
🚧 A graph-based core for a dependently typed language. 🚧

# 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

Programmers are in a pickle! We write text that gets parsed into trees, that then gets converted into graphs, that then get turned back into streams of bits, sent to a processor (in the style of a PDP-11), that then turned into graphs again on the processor!

On the other hand, our languages let us down. Lambdas, Π-types, Σ-types, identity types, etc. are all kind of annoying because they fix the ordering of parameters/arguments in prematurely, hiding away the 'graph'y structure of terms and types. What if we could defer the decisions of ordering till later?

## Examples

Note: This core language is not intended for direct manipulation! It's very verbose! It could however form the foundation of a projectional editor.

### Basic combinators

Some examples of simple combinators:

``````{ out identity
: [ in A = \$A : Type
, in a = \$_ : \$A
, out a = \$_ : \$A
]
= { in A = \$_
, in a = \$a
, out a = \$a
}
, out always
: [ in A = \$A : Type
, in B = \$B : Type
, in a = \$_ : \$A
, in b = \$_ : \$B
, out a = \$_ : \$A
]
= { in A = \$_
, in B = \$_
, in a = \$a
, in b = \$_
, out a = \$a
}
, out compose
: [ in A = \$A : Type
, in B = \$B : Type
, in C = \$C : Type
, in a-b = \$_ : [ in a = \$_ : \$A, out b = \$_ : \$B ]
, in b-c = \$_ : [ in b = \$_ : \$B, out c = \$_ : \$C ]
, out a-c = \$_ : [ in a = \$_ : \$A, out c = \$_ : \$C ]
]
= { in A = \$_
, in B = \$_
, in C = \$_
, in a-b = \$a-b
, in b-c = \$b-c
, out a-c
= { in a = \$a
, out c = \$c
, \$a-b ( a = \$a, b = \$b )
, \$b-c ( b = \$b, c = \$c )
}
}
, out subst
: [ in A = \$A : Type
, in B = \$B : Type
, in C = \$C : Type
, in a-b-c = \$_ : [ in a = \$_ : \$A, in b = \$_ : \$B, out c = \$_ : \$C ]
, in a-b = \$_ : [ in a = \$_ : \$A, out b = \$_ : \$B ]
, out a-c = \$_ : [ in a = \$_ : \$A, out c = \$_ : \$C ]
]
= { in A = \$_
, in B = \$_
, in C = \$_
, in a-b-c = \$a-b-c
, in a-b = \$a-b
, out a-c
= { in a = \$a
, out c = \$c
, \$a-b-c ( a = \$a, b = \$b, c = \$c )
, \$a-b ( a = \$a, b = \$b )
}
}
}
``````

### Fancy combinators

Some examples of fancy combinators with dependencies in their parameters:

``````{ out dependent-compose
: [ in A = \$A : Type
, in a-B = \$a-B : [ in a = \$_ : \$A, out B = \$_ : Type ]
, in a-b-C = \$a-b-C
: [ in a = \$a : \$A
, in b = \$_ : \$B
, out C = \$_ : Type
, \$a-B ( a = \$a, B = \$B )
]
, in a-b = \$_
: [ in a = \$a : \$A
, out b = \$_ : \$B
, \$a-B ( a = \$a, B = \$B )
]
, in a-b-c = \$_
: [ in a = \$a : \$A
, in b = \$b : \$B
, out c = \$_ : \$C
, \$a-B ( a = \$a, B = \$B )
, \$a-b-C ( a = \$a, b = \$b, C = \$C )
]
, out a-c = \$_
: [ in a = \$a : \$A
, out c = \$_ : \$C
, \$a-b ( a = \$a, b = \$b )
, \$a-b-C ( a = \$a, b = \$b, C = \$C )
]
]
= { in A = \$_
, in a-B = \$_
, in a-b-C = \$_
, in a-b = \$a-b
, in a-b-c = \$a-b-c
, out a-c
= { in a = \$a
, out c = \$c
, \$a-b ( a = \$a, b = \$b )
, \$a-b-c ( a = \$a, b = \$b, c = \$c )
}
}
, out dependent-subst
: [ in A = \$A : Type
, in a-B = \$a-B : [ in a = \$_ : \$A, out B = \$_ : Type ]
, in a-b-C = \$a-b-C
: [ in a = \$a : \$A
, in b = \$_ : \$B
, out C : Type
, \$a-B ( a = \$a, B = \$B )
]
, in a-b-c = \$_
: [ in a = \$a : \$A
, in b = \$b : \$B
, out c = \$_ : \$C
, \$a-B ( a = \$a, B = \$B )
, \$a-b-C ( a = \$a, b = \$b, C = \$C )
]
, in a-b = \$_
: [ in a = \$a : \$A
, out b = \$_ : \$B
, \$a-B ( a = \$a, B = \$B )
]
, out a-c
: [ in a = \$a : \$A
, out c = \$_ : \$C
, \$a-b ( a = \$a, b = \$b )
, \$a-b-C ( a = \$a, b = \$b, C = \$C )
]
]
= { in A = \$_
, in a-B = \$_
, in a-b-C = \$_
, in a-b-c = \$a-b-c
, in a-b = \$a-b
, out a-c
= { in a = \$a
, out c = \$c
, \$a-b-c ( a = \$a, b = \$b, c = \$c )
, \$a-b ( a = \$a, b = \$b )
}
}
}
``````

### Game data

``````{ out settings
: [ out window = \$_
: [ out width = \$_ : U32
, out height = \$_ : U32
, out is-fullscreen = \$_ : Bool
]
]
= { out window
= { out width = 400
, out height = 600
, out is-fullscreen = true
}
}
}
``````

### Mathematical structures

``````{ out Semigroup
: Type
= [ out Carrier = \$Carrier : Type
, out append = \$_
: [ in left : \$Carrier
, in right : \$Carrier
, out result : \$Carrier
]
]
, out Monoid
: Type
= [ out Carrier = \$Carrier : Type
, out empty = \$_ : \$Carrier
, out append = \$_
: [ in left : \$Carrier
, in right : \$Carrier
, out result : \$Carrier
]
]
}
``````

## Syntax

`label`s are the external names that we use to interact with terms and types.

`name`s (identifiers with `\$` signs in front) are internal names that allow us to 'wire up' our graphs. They should ultimately be auto-generated, but we make them human-readable in our examples. The name `\$_` is uses where the name is not used in the graph.

``````term ::=
| '[' type-entry* ']'                   type formation
| '{' term-entry* '}'                   term introduction
| 'Type'                                type of types
| name                                  variables

type-entry ::=
| 'in' label '=' name ':' term          input parameter
| 'out' label '=' name ':' term         output parameter
| name '(' (label '=' term)* ')'        term elimination

term-entry ::=
| 'in' label '=' name                   input parameter
| 'out' label '=' term                  output parameter
| name '(' (label '=' term)* ')'        term elimination
``````

TODO

TODO

## Questions

• What are the formation, introduction, and elimination rules?
• How do we normalize this and do conversion checking efficiently?
• Could this be extended to support 'very dependent types', or 'insanely dependent types' by lifting the syntactic restrictions on `out`put entries?
• Could we break up type graph formation and term graph introduction into more rudimentatary operations on graphs like in Algebraic Graphs with Class?
• Can we decorate these graphs with modal necessity/possibility in order to describe coeffects/effects like in Granule?
• How do we represent:
• disjoint unions? (Perhaps add `;` like in Mercury?)
• identity/path types?
• co-inductive types?
• nominal types?

## Inspiration/related work

### brendanzab commented Apr 15, 2020

 Alternate notation: ``````{ out identity : [ in A = 'A : Type, in a : 'A, out a : 'A, ] = { in A, in a = 'a, out a = 'a, }, out always : [ in A = 'A : Type, in B = 'B : Type, in a : 'A, in b : 'B, out a : 'A, ] = { in A, in B, in a = 'a, in b, out a = 'a, }, out compose : [ in A = 'A : Type, in B = 'B : Type, in C = 'C : Type, in a-b : [ in a : 'A, out b : 'B ], in b-c : [ in b : 'B, out c : 'C ], out a-c : [ in a : 'A, out c : 'C ], ] = { in A, in B, in C, in a-b = 'a-b, in b-c = 'b-c, out a-c = { in a = 'a, out c = 'c, 'a-b ( a = 'a, b = 'b ), 'b-c ( b = 'b, c = 'c ), }, }, out subst : [ in A = 'A : Type in B = 'B : Type, in C = 'C : Type, in a-b-c : [ in a : 'A, in b : 'B, out c : 'C ], in a-b : [ in a : 'A, out b : 'B ], out a-c : [ in a : 'A, out c : 'C ], ] = { in A, in B, in C, in a-b-c = 'a-b-c, in a-b = 'a-b, out a-c = { in a = 'a, out c = 'c, 'a-b-c ( a = 'a, b = 'b, c = 'c ), 'a-b ( a = 'a, b = 'b ), }, }, } ``````