Meaning-preserving modularity in a propositions-as-types style.

gistfile1.txt

// Meaning-preserving modularity in a propositions-as-types style.

// I've now posted about this code sample on my blog, and I'll leave
// this Gist the way it is (har har).
//
// This Gist: https://gist.github.com/4559120
//
// The blog post:
// http://rocketnia.wordpress.com/2013/01/29/an-extensible-type-system-for-meaning-preserving-modularity/


// Start of a bibliography:
//
// http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf
// http://twelf.org/wiki/Canonical_form
// http://arxiv.org/pdf/1201.5240v2.pdf
// http://www.mpi-sws.org/~dreyer/papers/proposal/proposal.ps
// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.7073
// http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
// http://www.scala-lang.org/docu/files/IC_TECH_REPORT_200433.pdf
// http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957
// http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html
// http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf
// http://www.daimi.au.dk/~eernst/tool07/papers/maspeghi04-ernst.pdf



// ===== Deductive fragment ==========================================
//
// Underlies all other fragments, except maybe the action fragment.


// == Grammar ==

// NOTE: Where we would say (a) |- (b) --- (c) |- (d), a more explicit
// sequent calculus might say (Gamma; a) |- (b) --- (Gamma; c) |- (d).
// Our inference rules always universally quanify over a context of
// preexisting facts, and their entailments always assume those facts.

// NOTE: (by Ross Angle) Currently I'm bending over backwards to avoid
// defining a term "#Type" that represents the type of a type. It's my
// way to avoid the intuition that the logic should support
// "#Type : #Type" and become inconsistent. Besides, I'm not yet
// convinced that "here's a type" is the most interesting theorem a
// type object demonstrates, nor that general "for all types..."
// quantification is a particularly valuable abstraction tool.

// A root node:
INFERENCE_RULES ::= Rule*

Rule ::=| Entailment* "---" Entailment*  // deduction
Rule ::=| Term "~~>" Term  // beta reduction
Entailment ::=| ("(" Fact ")")*"," "|-" ("(" Fact ")")*","
Fact ::=| UserVar "@" UserKnowledge
UserKnowledge ::=| "##type" Term
UserKnowledge ::=| Term ":" Term
Term ::=| TermVar
Term ::=| "(" Term ")"
Term ::=| "(" TermVar ":" Term ")" "->" Term
Term ::=| "\" TermVar ":" Term "->" Term
Term ::=| Term Term
Term ::=| "(" "##type" TermVar ")" "->" Term
Term ::=| "\" "##type" TermVar "->" Term
Term ::=| Term "#\t" Term
Term ::=| "(=#Sigma" TermVar ":" Term ")" "*" Term
Term ::=| "\#sigma" "(" Term ":" Term ")" "*" Term
Term ::=| "#fst" Term
Term ::=| "#snd" Term
UserVar ::= Word | "me" | "you"
TermVar ::= Word
// NOTE: This is the grammar of nonempty sequences of case-insensitive
// ASCII letters. When another grammar is specified as an alternation
// of this one and several particular examples, those examples are the
// only instances we actually use for that grammar in this document.
Word ::= ...

// Only for inference rules, not code:
Term ::=| TermVar ("[" Term "]")+

// Shorthands:
Entailment ::=| Fact  // short for |- (fact)
Term ::=| Term "->" Term  // short for ((x : term1) -> term2)
Term ::=| Term "*" Term  // short for ((=#Sigma x : term1) * term2)
Term ::=| "#Bottom"  // short for ((##type r) -> r)
Term ::=| "#Unit"  // short for ((##type r) -> r -> r)
Term ::=| "#unit"  // short for (\##type rType -> \r : rType -> r)
Term ::=| Term "||" Term
    // short for ((##type r) -> (term1 -> r) -> (term2 -> r) -> r)
Term ::=| "#left" Term Term Term
    // short for
    // (\##type r -> \a : (term1 -> r) -> \b : (term2 -> r) ->
    //     a term3)
Term ::=| "#right" Term Term Term
    // short for
    // (\##type r -> \a : (term1 -> r) -> \b : (term2 -> r) ->
    //     b term3)
Term ::=| "#Bool"  // short for (#Unit || #Unit)
Term ::=| "#true"  // short for (#left #Unit #Unit #unit)
Term ::=| "#false"  // short for (#right #Unit #Unit #unit)


// == Inference rules ==

// TODO: Prove a cut elimination theorem or something for all of this.

// Introduce \_:_->_ and (_:_)->_.
me @ ##type xType
(me @ x1 : xType)
    |- (me @ ##type yType[ x1 ]), (me @ y[ x1 ] : yType[ x1 ])
---
me @ ##type ((x2 : xType) -> yType[ x2 ])
me @ (\x3 : xType -> y[ x3 ]) : ((x4 : xType) -> yType[ x4 ])

// Eliminate (_:_)->_ and introduce _ _.
me @ f : ((x : xType) -> yType[ x ])
me @ xExample : xType
---
me @ f xExample : yType[ xExample ]

// Eliminate \_:_->_ and _ _.
(\x : xType -> y[ x ]) xExample
~~>
y[ xExample ]

// Introduce \##type_->_ and (##type_)->_.
(me @ ##type x1)
    |- (me @ ##type yType[ x1 ]), (me @ y[ x1 ] : yType[ x1 ])
---
me @ ##type ((##type x2) -> yType[ x2 ])
me @ (\##type x3 -> y[ x3 ]) : ((##type x4) -> yType[ x4 ])

// Eliminate (##type_)->_ and introduce _#\t_.
me @ f : ((##type x) -> yType[ x ])
me @ ##type xExample
---
me @ f #\t xExample : yType[ xExample ]

// Eliminate \##type_->_ and _#\t_.
(\##type x -> y[ x ]) #\t xExample
~~>
y[ xExample ]

// Introduce (=#Sigma_:_)*_ and #sigma_:_*_.
me @ ##type xType
(me @ x1 : xType) |- (me @ ##type yType[ x1 ])
me @ x2 : xType
me @ y[ x2 ] : yType[ x2 ]
---
me @ ##type ((=#Sigma x3 : xType) * yType[ x3 ])
me @ (\#sigma x2 : xType * y[ x2 ]) :
    ((=#Sigma x4 : xType) * yType[ x4 ])

// Eliminate (=#Sigma_:_)*_.
me @ s : ((=#Sigma x : xType) * yType[ x ])
---
me @ #fst s : xType
me @ #snd s : yType[ #fst s ]

// Eliminate \#sigma(_:_)*_ and #fst_.
#fst (\#sigma (x : xType) * y[ x ])
~~>
x

// Eliminate \#sigma(_:_)*_ and #snd_.
#snd (\#sigma (x : xType) * y[ x ])
~~>
y[ x ]



// ===== Observational subtyping fragment ============================
//
// Depends on the deductive fragment.

// This is essentially the equality constructed in "Observational
// Equality, Now!" However, we don't necessarily intend to treat it as
// a symmetrical judgment.


// == Grammar ==

Term ::=| Term "<==" Term  // subtype
Term ::=| "(" Term ":" Term ")" "<=" "(" Term ":" Term ")"
    // value equivalence across a subtype coercion
Term ::=| "#coerce" Term Term Term Term
Term ::=| "#coherent" Term Term
// NOTE: We need #typeRefl and #valRefl in order to prove
// self-equality of encapsulated or otherwise non-deductive types and
// values.
// TODO: Figure out what else we need. Maybe we need to know that
// equal values passed to equal functions yield equal results.
Term ::=| "#typeRefl" Term
Term ::=| "#valRefl" Term


// == Inference rules ==

me @ ##type a
me @ ##type b
---
me @ ##type (a <== b)

me @ a : aType
me @ b : bType
---
me @ ##type ((a : aType) <= (b : bType))

me @ pf : (a <== b)
me @ x : a
---
me @ #coerce a b pf x : b
me @ #coherent pf x : ((x : a) <= (#coerce a b pf x : b))

me @ ##type a
---
me @ #typeRefl a : (a <== a)

me @ x : a
---
me @ #valRefl x : ((x : a) <= (x : a))

#coerce ((ax1 : ai) -> ao[ ax1 ]) ((bx1 : bi) -> bo[ bx1 ]) pf orig
~~>
\bx2 : bi ->
    (#coerce ao[ #coerce bi ai (#fst pf) bx2 ]
        bo[ bx2 ]
        (#snd pf bx2 (#coerce bi ai (#fst pf) bx2)
            (#coherent (#fst pf) bx2))
        (orig (#coerce bi ai (#fst pf) bx2)))

((ax1 : ai) -> ao[ ax1 ]) <== ((bx1 : bi) -> bo[ bx1 ])
~~>
(bi <== ai) *
    ((bx2 : bi) -> (ax2 : ai) -> ((bx2 : bi) <= (ax2 : ai)) ->
        (ao[ ax2 ] <== bo[ bx2 ]))

(a : ((ax1 : ai) -> ao[ ax1 ])) <= (b : ((bx1 : bi) -> bo[ bx1 ]))
~~>
(ax2 : ai) -> (bx2 : bi) -> ((ax2 : ai) <= (bx2 : bi)) ->
    ((a ax2 : ao[ ax2 ]) <= (b bx2 : bo[ bx2 ]))

#coerce ((##type ax) -> ao[ ax ]) ((##type bx) -> bo[ bx ]) pf orig
~~>
\##type x -> (#coerce ao[ x ] bo[ x ] (pf #\t x) (orig #\t x))

((##type ax) -> ao[ ax ]) <== ((##type bx) -> bo[ bx ])
~~>
(##type x) -> (ao[ x ] <== bo[ x ])

(a : ((##type ax) -> ao[ ax ])) <= (b : ((##type bx) -> bo[ bx ]))
~~>
(##type x) -> ((a #\t x : ao[ x ]) <= (b #\t x : bo[ x ]))

#coerce ((=#Sigma ax1 : ai) * ao[ ax1 ])
    ((=#Sigma bx1 : bi) * bo[ bx1 ])
    pf orig
~~>
\#sigma (#coerce ai bi (#fst pf) (#fst orig) : bi) *
    (#coerce ao[ #fst orig ]
        bo[ #coerce ai bi (#fst pf) (#fst orig) ]
        (#snd pf (#fst orig) (#coerce ai bi (#fst pf) (#fst orig))
            (#coherent (#fst pf) (#fst orig)))
        (#snd orig))

((=#Sigma ax1 : ai) * ao[ ax1 ]) <== ((=#Sigma bx1 : bi) * bo[ bx1 ])
~~>
(ai <== bi) *
    ((ax2 : ai) -> (bx2 : bi) -> ((ax2 : ai) <= (bx2 : bi)) ->
        (ao[ ax2 ] <== bo[ bx2 ]))

(a : ((=#Sigma ax1 : ai) * ao[ ax1 ])) <=
    (b : ((=#Sigma bx1 : bi) * bo[ bx1 ]))
~~>
((#fst a : ai) <= (#fst b : bi)) *
    ((#snd a : ao[ #fst a ]) <= (#snd b : bo[ #fst b ]))



// ===== Action fragment =============================================


// == Grammar ==

// A root node:
MODULE ::= UserAction*

Fact ::=| UserVar "@!" UserAction
// NOTE: This is a user's knowledge that they have the choice to
// perform an action.
UserKnowledge ::=| UserAction

// Only for depictions of external modules, not inference rules or
// actionable module code:
Term ::=| "#<hiddenCode>"


// == Inference rules ==

// (none)



// ===== Local collaboration fragment ================================
//
// Depends on the deductive fragment and the action fragment.


// == Grammar ==

UserKnowledge ::=| "##secret" Key
UserKnowledge ::=| "##public" Key
Key ::=| KeyVar
KeyVar ::= Word | "myKey" | "yourKey" | "from" | "to" | "by" | "key"

// Only for code, not inference rules:
Key ::=| "$" ## CryptographicKeyName
Key ::=| "$$everyone"
Key ::=| Key ## "/" ## SubName
CryptographicKeyName ::= ExternallyVisibleWord
SubName ::= ExternallyVisibleWord
// NOTE: In any place this grammar is used, an actual programming
// language implementation is very likely to use a different format.
// Sequences of ASCII letters aren't a very conscientious
// international standard.
ExternallyVisibleWord ::= Word


// == Inference rules ==

// (none)



// ===== Local collaborative value-level definition fragment =========
//
// Depends on the local collaboration fragment.


// == Grammar ==

UserAction ::=| "!!define" Key Key Term Term
Term ::=| "#the" Key Key Term


// == Inference rules ==

// Introduce !!define.
me @ ##secret myKey
me @ ##public yourKey
me @ ##type xType
me @ x : xType
---
me @ !!define myKey yourKey xType x

// Eliminate !!define and introduce #the.
me @! !!define myKey yourKey xType x
you @ ##public myKey
you @ ##secret yourKey
you @ ##type xType
---
you @ #the myKey yourKey xType : xType



// ===== Local collaborative phantom type fragment ===================
//
// Depends on the local collaboration fragment.


// == Grammar ==

UserAction ::=| "!!defineWrapper" Key Term
Term ::=| "#Wrapper" Key
Term ::=| "#wrap" Key Term
Term ::=| "#unwrap" Key Term
// TODO: Figure out what else we might need in order to reason about
// equality of wrapped values.


// == Inference rules ==

// Introduce #Wrapper.
me @ ##public by
---
me @ ##type (#Wrapper by)

// Introduce !!defineWrapper.
me @ ##secret by
me @ ##type innerType
---
me @ !!defineWrapper by yourKey innerType

// Eliminate !!defineWrapper and introduce #wrap.
me @! !!defineWrapper by innerType
me @ ##secret by
me @ ##type innerType
---
me @ #wrap by innerType : innerType -> #Wrapper by

// Eliminate !!defineWrapper and introduce #unwrap.
me @! !!defineWrapper by innerType
me @ ##secret by
me @ ##type innerType
---
me @ #unwrap by innerType : #Wrapper by -> innerType



// ===== Local collaborative extensible sum fragment =================
//
// Depends on the local collaboration fragment and the observational
// subtyping fragment.

// A certain user action can establish a new extensible sum type along
// with a policy on how that type can be extended. Another user can
// extend that sum with new cases, but only if they provide a way to
// preserve that policy, even in spite of others' independent ability
// to extend the sum.
//
// In a more user-friendly language, it may appear that several
// interdependent extensible sums and policies can be declared
// together in a bundle. However, that can probably be implemented on
// top of this single-sum, single-policy system.
//
// This system introduces a certain kind of infinity: Say one user
// starts a new extensible sum type (#SumPart myKey). Another user
// extends it, but their extension family's index (i.e. newParts) is
// of type (#SumPart myKey) itself, or of some related type, so now
// the inhabitants (#SumPart myKey) go into an infinite regress.
//
// TODO: See if that infinite regress leads to an embedding of
// inductive and/or coinductive definitions, or if it even leads to
// logical inconsistency.


// == Grammar ==

UserKnowledge ::=| "##extensible" Term
UserAction ::=| "!!startSum" Term TermVar Term Term TermVar Term
UserAction ::=| "!!youCanExtendSum" Key Key TermVar Term
UserAction ::=| "!!extendSum" Key Key Term TermVar Term
Term ::=| "#SumPart" Key
Term ::=| "#sumExt" Key Key
Term ::=| "#sumExtElim" Key Key
Term ::=| "#Extend" Term Term
Term ::=| "#stoe" Term Term
Term ::=| "#etos" Term Term
Term ::=| "#extend" Term Term
// TODO: Figure out what else we might need in order to reason about
// equality of these values.


// == Inference rules ==

// Introduce #SumPart.
me @ ##public by
---
me @ ##type (#SumPart by)

// Introduce !!startSum.
me @ ##secret myKey
me @ ##type seedParts
(me @ ##type x1) |- (me @ ##type accum[ x1 ])
(me @ ##type e1), (me @ ##extensible e1) |-
    (me @ seedImplementation[ e1 ] : accum[ #Extend seedParts e1 ])
---
me @ !!startSum
    myKey x2 accum[ x2 ] seedParts e2 seedImplementation[ e2 ]

// Eliminate !!startSum and introduce #sumExt, #sumExtElim, and
// #sumOut.
me @!
    !!startSum myKey x accum[ x ] seedParts e seedImplementation[ e ]
---
me @ #sumExt myKey myKey : seedParts -> #SumPart myKey
me @ #sumExtElim myKey myKey : #SumPart myKey -> (seedParts || #Unit)
me @ #sumOut myKey : accum[ #SumPart myKey ]

// Eliminate !!startSum and introduce !!youCanExtendSum.
//
// TODO: See if we actually need to share accum[ x ] itself or if we
// can share less information while still making it just as possible
// to formulate an extension.
//
// TODO: See if we need to send an abstracted version of accum[ x ] in
// order to make certain kinds of extension invariants possible to
// enforce.
//
me @! !!startSum
    myKey x1 accum[ x1 ] seedParts e seedImplementation[ e ]
me @ ##public yourKey
---
me @ !!youCanExtendSum myKey yourKey x2 accum[ x2 ]

// Eliminate !!youCanExtendSum and introduce !!extendSum.
//
// TODO: The point of incorporating "#SumPart myKey" is so we can take
// full advantage of preexisting definitions related to this sum when
// making an extension. See if this approach fully accomplishes this
// goal, and see if its circularity somehow leads to inconsistency.
//
// NOTE: We're having <== indicate a proof that there's exactly one
// way to coerce, so that it stays proof-irrelevant. However, we're
// using <= to indicate that a value of one type supports no more
// observations than another value of another type. If we let <== be
// computationally relevant, extend[ e ] could just be a <== proof.
//
me @! !!youCanExtendSum myKey yourKey x1 accum[ x1 ]
you @ ##public myKey
you @ ##secret yourKey
you @ ##type myParts
(you @ ##type x2) |- (you @ ##type accum[ x2 ])
(you @ ##type e1), (you @ ##extensible e1) |-
    (you @ extend[ e1 ] :
        ((x : accum[ #Extend (#SumPart myKey) e1 ]) ->
            (=#Sigma y : accum[ #Extend myParts
                (#Extend (#SumPart myKey) e1) ]) *
                ((x : accum[ #Extend (#SumPart myKey) e1 ]) <=
                    (y : accum[ #Extend myParts
                        (#Extend (#SumPart myKey) e1) ]))))
---
you @ !!extendSum myKey yourKey myParts e2 extend[ e2 ]

// Eliminate !!extendSum and introduce #sumExt and #sumExtElim.
you @! !!extendSum myKey yourKey myParts e extend[ e ]
---
you @ #sumExt myKey yourKey : myParts -> #SumPart myKey
you @ #sumExtElim myKey yourKey : #SumPart myKey -> (myParts || #Unit)

// Introduce #Extend, #stoe, #etos, and #extend.
me @ ##type myParts
me @ ##extensible e
---
me @ ##type (#Extend myParts e)
me @ #stoe myParts e : ((myParts || e) -> #Extend myParts e)
me @ #etos myParts e : (#Extend myParts e -> (myParts || s))
me @ #extend myParts e : ((x : e) -> (#=Sigma y : #Extend myParts e) *
    ((x : e) <= (y : #Extend myParts e)))

// TODO: See if #extend is enough to actually prove the things we need
// to prove for !!extendSum. We might not have transitivity of <= yet,
// or something.



// TODO: Consider adding another approach to extensible sum types,
// which would be well integrated with the idea of knowledge queries,
// but not so well integrated with the deductive system:
//
// Term ::=| "#K" Term
// Term ::=| "#defined" Key Key
// Term ::=| "#letKnown" TermVar Term Term
// UserAction ::=| "!!letKnown" TermVar Term UserAction
//
// A judgment "x : #K t" says x would terminate as evidence for t if
// all possible knowledge were available for query purposes and all
// queries generated during execution of x turned out to be
// well-defined. The #K type constructor may syntactically be a monad,
// but it works more like an effect type, tainting the type of any
// function call that has it as a subexpression.
//
// The #letKnown and !!letKnown syntaxes perform knowledge queries.
// Instead of saying "#the from to type", we say
// "!!letKnown x (#defined from to type) (...)" around the
// top-level user action, and it will be fully resolved before the
// action is admitted into the network--or it will fail to complete,
// and the action won't take place. (Or should it be possible to
// publish this incompletely defined action and then do the knowledge
// queries on the observing user's side?)
//
// Term ::=| "#Mystery"
// Term ::=| "#mystery" Key Term
// Term ::=| "#dispatcher" Key
// UserAction ::=| "!!decideMysteryType" Key Term
// UserAction ::=| "!!startDispatcher" Key Term
// UserAction ::=| "!!extendDispatcher" Key Key Term
//
// If one person does "!!startDispatcher to resultType" and others do
// "!!decideMysteryType from inputType" and
// "!!extendDispatcher from to func", with each "func" of type
// (inputType -> #K resultType), then the person who started the
// dispatcher has access to a value "#dispatcher to" of type
// (#Mystery -> #K resultType). Values of type #Mystery will dispatch
// to the method defined on the same key that created them.



// ===== Example built-in module: Natural numbers ====================

!!define $language/natZero $$everyone
    (#Wrapper $language/nat)
    #<hiddenCode>
!!define $language/natSucc $$everyone
    (#Wrapper $language/nat -> #Wrapper $language/nat)
    #<hiddenCode>
!!define $language/natElim $$everyone
    ((##type a) -> #Wrapper $language/nat -> a -> (a -> a) -> a)
    #<hiddenCode>