Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
🚧 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

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

Semantics

TODO

Typing

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 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?

Inspiration/related work

@brendanzab

This comment has been minimized.

Copy link
Owner Author

@brendanzab 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 ),
        },
    },
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.