Bayle Shanks's website: proj-oot-old-150618-ootNotes4

huh, this looks very general, clean, and like the keywordish relations that i've been looking for:

http://www.lshift.net/blog/2010/12/22/conditional-statements-the-lambda-calculus-and-earlylate-binding

" Conditionals in Smalltalk work like this: the class Boolean has two subclasses, True and False. Each has a well-known instance, true and false, respectively [2].

The equivalent of C’s

  if (condition) {
    onefunc();
  } else {
    otherfunc();
  }

  condition
    ifTrue: [ self oneMethod ]
    ifFalse: [ self anotherMethod ]

How does it work? Boolean defines a method #ifTrue:ifFalse: taking two blocks as parameters. (Remember, what Smalltalkers call a block other folks call a closure. A Lisper might call the parameterless blocks that #ifTrue:ifFalse: takes thunks.) True and False in turn implement #ifTrue:ifFalse: thusly:

  True>>ifTrue: trueBlock ifFalse: falseBlock
    ^ trueBlock value.

False>>ifTrue: trueBlock ifFalse: falseBlock ^ falseBlock value.

So we evaluate condition to either true or false, send it the #ifTrue:ifFalse: message, and we’re done. "

---

Disciple exceptions: " The exception mechanism in the source language is based around try/catch, and doesn't have a proper semantics. We should probably just use the GHC approach where the 'error' function creates an exceptional value instead of causing a side effect.

    If we were going to treat exceptions as side effects, then perhaps we could do something like in Benton and Buchlovsky's "Semantics of an effect analysis for exceptions" paper. "

---

" The network is reliable.

    Latency is zero.

    Bandwidth is infinite.

    The network is secure.

    Topology doesn't change.

    There is one administrator.

    Transport cost is zero.

    The network is homogeneous."

    Structured programming (in a first-order language) limits a program’s control flow graph to being constructed using a particular grammar, which makes it easier to understand what are the potential control traces in a program.
    Data hiding (encapsulation) limits which modules may access the representation of an abstract type, which means that in other modules we can reason in terms of a simpler interface, and when inside the abstraction boundary we can assume the unprivileged modules rely only on the external interface.
    Immutability prevents objects from being modified by other modules or processes, which eases reasoning about concurrency and time, and allows us not to think about how another module might modify objects that we share with it.
    Purely functional programming goes further than immutability, eliminating non-local information flows, which means that we can understand expressions in terms of their text and lexical environment, and ignore time in extensional reasoning.
    Static types constrain which types of values can flow where, which means that there are fewer possibilities to think about in case analyses, and particular kinds of errors need not be considered."

---

[esq-ue tu speak Oot](query, desired type of response=bool)

---

the words "I" and "you"

hypotheticals

a way of making a request, that is, of indicating the desired response

a way to say what someone [i or you, or someone else] known or what is unknown to them [and, branching off 'know', we then have more complex concepts such as 'understand']

a way to indicate an object, not by a noun phrase, but by specifying some properties about it, 'the thing which was here yesterday', for example

past and future tense?

plurality?

of course, there are different levels of interpretation; if text is quoted, 'i' and 'you' are unresolved, otherwise they are ('i' relative to 'speaker', 'you' relative to 'listener')

kant's correspondance between table of judgement and categories may be useful for uniform notation; e.g. coq's and haskell's definition of data types/constructors by cases == OR in the same way that disjunctive judegment == community (i think), and kant's hypothetical == causation link tells us that we can reuse the symbol for 'if' for 'right arrow' e.g. the horn connective (possibly this is also the same as the symbol for subtyping, too, e.g. ontological logic? see what descriptive logic does there)

the difference between 'i' and 'me' is like the different roles in a relation; the relation is like the very (look at RDF), and subject/object are roles (positions in the relational operator)

as one task (but not the only task) of philosophy is to form new language, programming language creation is rather philosophical

the Curry-Howard Isomorphism is somewhat related to Kant's relationship between the table of judegments and the categories

for example, union sum types mean a type where you don't know exactly which type you have, but you know you have one of the ones on the list. this is like Kant's category of Community. union sum types are related to logical disjunction; this is like Kant relating them to Disjunctive judgements.

in other words, Kant's relationship between the table of judegments and the categories is like the relationship between the logic of types (e.g. 'disjunction' for a union type), and their meaning as types (e.g. 'you have one of these types but you don't know which'), which is like the relationship described at http://web.archive.org/web/20130702221947/http://www.haskell.org/haskellwiki/GADTs_for_dummies between normal Haskell code, and what typeclasses would look like if expressed in a uniform notation with normal Haskell code

by this logic, an 'implication' type would indeed seem to be subtyping, e.g. 'Q -> P' means' 'not(Q) OR P' which is equal to 'not(Q) OR (Q AND P)'. Consider the relationship between Q=Integer, P=Number. Either something is not an integer, or you assume that it is both an integer and a number.

todo why is subtyping hard when it interacts with polymorphism?

substance, e.g. essential vs. accidental properties:

(a) in class-based OOP systems we have this distinction, in prototype-based ones we don't

the idea that everything is of some single type of 'substance' is like single inheritance

(b) one might also relate it to what is statically known (although this is a slightly different idea than (a)); essential properties can be statically known, accidental ones cannot.

(c) how to apply this to EverythingIsAnInterface?? First, think of multiple inheritance. We can generalize the idea of essential properties as being those that are part of 'the' substance, to saying that an object (a piece of data) has multiple substances, each of which carry/imply various essential properties. Second, realize that really what we are doing here is making an epistemological distinction; if and only if the reason that we know that an object has a given attribute is due to it being a substance, then we call that attribute 'essential'. This lets us see that in this case interfaces are like classes with respect to methods specified in the interface.

In fact, this means that which attributes are essential and which are accidental is relative to what we consider to be substances. In one context (say, serializing an object), we might not know that the object under examination supports the 'dict' interface, all we know is that it has a function called 'keys' attached to it. In this context, 'keys' is an accidental property. In another context, we might know that a given variable must contain an object of type 'dict'; in this context, the 'keys' function is an essential property of that variable.

(b) is explained as the context of dynamic languages by saying that it's not whether something is STATICALLY known, it's whether it is a property of an object's TYPE.

in the structural typing context of Oot, typing is (mostly? or totally? what about type labels and the .types meta attribute?) equivalent to pattern matching. so essential/accidental is not so much about compile-time/run-time but about whether you may assume something because you've required it to be matchable against a pattern.

this kind of thinking probably should inform what we decide about class vs. prototype inheritance

btw the wording that "a substance IMPLIES various essential properties" is further support for the implication-as-subtyping

todo why is subtyping hard when it interacts with polymorphism?

" Subtyping and type inference

The type inference problem in the presence of parametric polymorphism and subtyping like in Java and C# is significantly harder than in Haskell (98) or SML. You're very unlikely to ever get anything like those FP languages' type inference. Scala is a good language to look at in this regard. It too uses (only) local type inference which is more or less as much as one can reasonably expect. That said, you can do way, way more with local type inference than C# is doing (as Scala demonstrates.) " -- http://lambda-the-ultimate.org/node/2862

" .. You ought to formalize the 'laws' of this particular graph theory, and explain it with node/edge diagrams and examples.

Definitely! I have one heck of a conference paper to write about this. It doesn't help that much of the existing type theory out there is based on term structure, not graph theory. However, I've done this before for Jiazzi, so I think its doable. It also turns out that any type theory that involves nominative subtyping is also based on some amount of graph theory. .. " -- http://lambda-the-ultimate.org/node/4764

inferred row polymorphism?

This seems to be an extension of the concept of row polymorphism to type/object/state inheritance and construction (read as a complement; I like extensions of excellent systems). That is, where row polymorphism accepts use site variance, YinYang? treats it as a point of assertion, constructing the structural definition from the implicit name-use constraints. YinYang? does for specification-definitional simplicity what RP does for use-site specification.

Then again, I've fallen for row polymorphism recently so I'm seeing its face in every crowd. Does somebody have a distinction between the systems I'm missing? By Chad Wellington at Wed, 2013-06-19 01:31

That is a quite useful

That is a quite useful comparison. I don't think YinYang? is very close to row polymorphism because it is completely nominative, but I'll try to learn more about the topic to be sure. By Sean McDirmid? at Wed, 2013-06-19 09:49

An explanation, sadly long-winded

Here's the analogy that I saw, with apologies in advance: (1) I'm very good at mixing up (mixing in?) concepts under names that are inappropriate, (2) I think in Lisp syntax so I'm not quite following your YinYang? syntactic conventions, and (3) this ended up a lot longer than I'd hoped.

From your YinYang? post: "what class an object extends depends on what it does" The analogous Row Polymorphism style: "the elements required of input types depend on names used"

I have seen the view of row polymorphism that I would characterize as "implementation-oriented", where RP is an indexing trick to expose subsets of a product type. I.e., the type (a * b * c) would carry around the map (a->1, b->2, c->3) so that a use-site requiring (a * c) could look up the appropriate indices in the type it is handed.

I'm here using RP in terms of its type-requirements inference rather than its implementation. That is, seeing a function use (a * c) tells us that it can use any type exposing "a" and "c". To repeat the example from the post:

(def foo (a b) (+ a b)) ;

; for example (def

+	must be a function of a, b
+	(a b)

    (_add_ a.as_number b.as_number)); so now we know that "a" and "b" need an "as_number" named property ; thus, we can infer that "foo" is polymorphic over any types with "as_number" property

We can apply this kind of reasoning to the ThicknessListener? function:

(def ThicknessListener? (w) (if w.Pressed (assign w.Thickness 10) nil)) ; "w" must have "Pressed" and "Thickness" properties

deriving type (w: :(product Pressed Thickness))

What I see YinYang? as extending this RP-like name-polymorphism inference is the capability to infer construction, and not merely inferring possible uses. Thus, if we use the ThicknessListener? as so:

I see YinYang? extending this in two ways

    namespaced product types through the trait extension hierarchy
    inferred type construction

We can see the first (namespace names) in the trait definitions:

(defTrait Widget () ()) (defTrait Bordered (Widget) (Thickness : double)) (defTrait Button (Widget) (Pressed : bool))

These imply that the named-trait "Pressed" can only be inferred in some type already declared or inferred to be a "Widget". In RP, I might make a type (say, "Cylinder") with "Thickness:double" and "Pressed:bool" properties, referring to an actual physical object made of pressed metal rather than a graphical widget.

We can see the second (inferred construction) in this hacky use of the above:

(let (w (new Widget)) (assign w.Pressed false) (ThicknessListener? w) )

The ThicknessListener?