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.
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?
Note: This core language is not intended for direct manipulation! It's very verbose! It could however form the foundation of a projectional editor.
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 )
}
}
}
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 )
}
}
}
{ 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
}
}
}
{ 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
]
]
}
labels are the external names that we use to interact with terms and types.
names (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
- 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
output 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?
- disjoint unions? (Perhaps add
Alternate notation: