brendanzab

/-
  Total and partial maps

  This is inspired by [the relevant chapter in Software Foundations]. Unlike
  Software Foundations, these maps are also parameterised over a `Key`
  type, which must supply an implementation of `DecidableEq`.

  [Software Foundations]: https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
-/
namespace Maps

brendanzab

marp	theme
true	uncover

Pikelet status update

Brendan Zabarauskas

31/08/2020

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

% Copyright 2020 YesLogic Pty. Ltd.
%
% Licensed under the Apache License, Version 2.0 (the "License");
% you may not use this file except in compliance with the License.
% You may obtain a copy of the License at
%
%     http://www.apache.org/licenses/LICENSE-2.0
%
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS,

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

(* terms *)

term : type.

universe : term.
annotate : term -> term -> term.
unitType : term.
unitTerm : term.
pairType : term -> (term -> term) -> term.
pairTerm : term -> term -> term.

brendanzab

//! See [this twitter thread](https://twitter.com/brendanzab/status/1191233778854662144).
//!
//! Traditional syntax trees suffer from lots of pointer indirections and poor data locality!
//! Could we stream things instead, using [pull-based events](http://www.xmlpull.org/history/index.html)
//! as opposed to trees? This should be equivalent to our tree based approaches, but might
//! require us to think carefully about what our core calculus looks like in order to make
//! this kind of thing easier.

use std::sync::Arc;

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

//! Dependent type system that uses a SAX-style event streams between passes.
//!
//! It would be really neat to have a simple state machine language to describe this.

/// Handler for a state machine that accepts input events.
trait InputHandler {
    fn on_bytes(self, bytes: &[u8]>);
    fn on_list_start(self);
    fn on_list_end(self);
}