(Last modified 2011-12-03)
(i) ∀phrased = (* Υ Π) : σ,
∃purpose = (* Γ Π) : {* Γ Π}, such that (* Γ Π) = (* Υ Π) <T> (Υ _ Γ)
=>
∃!λ, ∃τ, such that ∃Auth : λ -> (σ -> τ), ∃Proc : σ -> λ and (Auth o Proc) = (Υ _ Γ)
or:
(ii) ∀phrased = (Π Υ *) : σ,
∃purpose = (Π Γ *) : {Π Γ *}, such that (Π Γ *) = (Π Υ *) <T> (Υ _ Γ)
=>
∃!λ, ∃τ, such that ∃Auth : λ -> (σ -> τ), ∃Proc : σ -> λ and (Auth o Proc) = (Υ _ Γ)
(More details below)
(Below, we exemplify our scheme/constructs in concrete syntax, via a hypothetical language extension to C#, when used as the host language, with relevant components/comments in bold.)
// Begin code sample
{#{
using <regard://markup@w3.org/TR/REC-xml> as XML
where <urn:w3.org:rec:xml-infoset> is infoset
where <urn:w3.org:rec:xml:entity:utf8> is utf8entity;
}#} // XML language design intent import and aliasing directive
//(some more vanilla C#...)
var xmlPayload = "<data />"; // usual C# type inference at work here => 'var xmlPayload = ...' <-> 'string xmlPayload = ...'
var purpose = (#( // start marker
XML // the assumed XML formal language alias, reified (in above directive) as a URI
( xmlPayload ) // note: one could also be using directly the string literal, as in '( "<data />" )'
infoset // the XML phrase (xmlPayload)'s purpose alias (from output PoV), reified (in above directive) as a URN
)#); // end marker; at this point, expression is typed: Func<'inferred-type'>
// it's mostly all about this new type inference scheme that things get more interesting below (read on...)
var infoset = purpose(); // usual strict (eager) or lazy evaluation of the purpose's value, in the host language (C#)'s type system
// Here, in context, previous line fundamentally replaces a call to some xmlDoc.LoadXml(...) (but many other use cases possible)
// End code sample
// Begin code sample
{#{
using <regard://markup@w3.org/TR/REC-xml> as XML
where <urn:w3.org:rec:xml-infoset> is infoset
where <urn:w3.org:rec:xml:entity:utf8> is utf8entity;
}#} // XML language design intent import and aliasing directive
//(some more vanilla C#...)
var xmlDoc = new XmlDocument(); // usual C# type inference at work here => 'var xmlDoc = ...' <-> 'XmlDocument xmlDoc = ...'
// (... e.g., some more work w/ xmlDoc, etc)
var purpose = (#(
utf8entity // the XML phrase's purpose alias (from input PoV), reified (in above directive) as a URN
( xmlDoc )
XML // the assumed XML formal language alias, reified (in above directive) as a URI
)#); // end marker; at this point, expression is typed: Func<'inferred-type'>
// it's mostly all about this new type inference scheme that things get more interesting below (read on...)
var xmlSource = purpose(); // usual strict (eager) or lazy evaluation of the purpose's value, in the host language (C#)'s type system
// Here, in context, previous line fundamentally replaces a read of xmlDoc.OuterXml (but many other use cases possible)
// End code sample
Time for first questions/answers probably:
(omitting the obvious questions which have almost-as-obvious answers, though)
Q)1: So, what is the 'inferred-type' for infoset in example (I) and for xmlSource in example (II), anyway?
A)1: Well, depends. But here, one could likely expect, for instance,
for (I): System.Xml.XmlDocument and
for (II): System.String
Q)2: Huh? How come you could answer A)1 that way?
A)2: That's the whole thing/point here. The infrastructure (REGARD URI scheme) + CLR/CTS platform + the compiler type inference algorithm
cooperate to figure this out for the programmer.
But...
Wait... Couldn't there be other opportunities to benefit from these STLC look-alike formulas up there?
Yes, there are, indeed. For instance, the example (I) above could have as well been written, instead:
// Begin code sample
{#{
using <regard://markup@w3.org/TR/REC-xml> as XML
where <urn:w3.org:rec:xml-infoset> is infoset
where <urn:w3.org:rec:xml:entity:utf8> is utf8entity;
}#} // XML language design intent import and aliasing directive
//(some more vanilla C#...)
// Note there is no more need here for declaring/binding the former C# identifier "xmlPayload" 's as reif. of the XML phrase in the CTS
var purpose = (#( XML // the assumed XML formal language alias, reified (in above directive) as a URI
{<?xml version="1.0" ?>
<data />
} // yes, an XML literal appearing in-situ, not only expressed in XML's normal syntactical form, but also coming with
// a semantic definition for acceptable reifications (i.e., representations in the host language's type sytem),
// depending on the usage the host language makes out of it, in this context, for the purpose given here
// (which is also reified, via a URN, in this same enonciation site).
// Note the use, in this context, of curly brackets to differentiate a Φ-literal embedding from a Γ-typed expression
// (enclosed in parentheses, in first two examples I. & II.).
infoset )#);
var infoset = purpose(); // // usual strict (eager) or lazy evaluation of the purpose's value, in the host language (C#)'s type system
// Here, in context, previous line fundamentally replaces a call to some xmlDoc.LoadXml(...) (but many other use cases possible)
// End code sample
More Q)uestions? ... if so, feel free to write me
Π : Language Phrase's Purpose
(as a URN in Υ)
Φ : Foreign Language (* Φ Π) : {* Φ Π}-Type ( λ )
(as a URI in Υ)
Γ : Φ's Host Language (* Γ Π) : {* Γ Π}-Type ( σ -> τ )
Υ : REGARD of Φ in Γ (* Υ Π) : {* Υ Π}-Type ( σ )
Auth : Φ language's authority Auth : {* Φ Π}-Type -> {* Γ Π}-Type ( λ -> (σ -> τ) )
Proc : current Γ processor Proc : {* Υ Π}-Type -> {* Φ Π}-Type ( σ -> λ )
(* Γ Π) = (* Υ Π) <T> (Υ _ Φ) <T> (Φ _ Γ) = (* Υ Π) <T> (Auth o Proc) : {* Γ Π}-Type ( σ -> τ )
∀phrased = (* Υ Π) : σ,
∃purpose = (* Γ Π) : {* Γ Π}, such that (* Γ Π) = (* Υ Π) <T> (Υ _ Γ)
=>
∃!λ, ∃τ, such that ∃Auth : λ -> (σ -> τ), ∃Proc : σ -> λ and (Auth o Proc) = (Υ _ Γ)
E.g., in C# FP-style:
proc_accepts == Proc
auth_reified == Auth
host_λ_ified = (auth_reified o proc_accepts) == (Auth o Proc) : σ -> (σ -> τ)
Assuming:
proc_accepts : λ delegate(σ phrased) // TBD...
auth_reified : Func<σ, τ> delegate(λ lphrase) // TBD...
host_λ_ified : Func<σ, τ> delegate(σ phrased) = (σ phrased) => auth_reified(proc_accepts(phrased))
Allows:
σ phrased = ...
τ purpose = host_λ_ified(phrased)(phrased)
Or also (after applying the Yoneda embedding / Continuation-Passing Style (CPS) Transform):
Assuming:
proc_accepts : λ delegate(σ phrased) // TBD...
auth_reified : Func<σ, τ> delegate(λ lphrase) // TBD...
host_λ_ified2 : Func<σ, τ> delegate(Func<λ, Func<σ, τ>> auth_reified, σ phrased) =
(Func<λ, Func<σ, τ>> auth_reified, σ phrased) => auth_reified(proc_accepts(phrased))
Allows:
σ phrased = ...
τ purpose = host_λ_ified2(auth_reified, phrased)(phrased)
Or also, finally:
Assuming:
proc_accepts == Id : σ -> σ = σ => σ (identity) i.e., we've chosen λ = σ, trivially, in Γ
Υ_URI_regard : Func<Uri, Uri, Func<σ, τ>> // (TBD) in essence: the REGARD infra queries Φ's authority about (* Φ Π)'s semantic in regard to Γ, i.e.: (* Γ Π)
host_λ_ified3 = (σ phrased) => Υ_URI_regard<σ, τ>(Φ, Π)(phrased)
Allows:
σ phrased = ...
Uri Φ = ... // Φ language's REGARD URI
Uri Π = ... // Π purpose's URN
τ purpose = host_λ_ified3(phrased)
(Last modified 2011-12-03)
© C.J., 2011.