proj-oot-ootLevelsNotes1

an example of the 'levels' concept is the difference between a view of the graph of the file directories where symbolic links are followed (lower level), and where they are not followed (higher level). abstracting from this, one type (or the only type?) of 'level' is where, at a lower level, some sort of metaprogramming device (e.g. symbolic links, e.g. __get's and __set's) is transparently active, and at a higher level, it is quoted. (actually, maybe i have higher and lower mixed up here? maybe metaprogramming should be active at a high level, but you can see the hidden machinery at a low level; e.g. then it's like higher and lower level programming languages)

--

Hoon says that it uses the %hold type, which afaict is like a generator function, to explicitly build patterns for infinite lists, rather than have the core language actually pretend that some lists are infinite.

the author of the language says that one advantage of this 'explicit laziness' over the 'implicit laziness' of languages like Haskell that hide the generator and allow the client only to see the seemingly infinite list that results, is that you can recurse into an explict lazy list and then halt when you are about to recurse into a generator that you have already seen:

" one advantage of explicit over implicit laziness...is that the explicit pattern state makes a good search key for an associative array, ie, ++map in Hoon. ... Consider the function computed by ++nest. Again simplifying the interesting core structure of ++ut, (nest sut ref) is yes if it can verify that every noun which is a member of type ref is also a member of type sut. In other words, ++nest is a conservative algorithm - it sometimes busts the innocent, it always nails the guilty. ... ++nest and everything else in the Hoon type system practice a policy of pure "structural equivalence .... If you look again at ++type above and forget about %hold, it is probably not hard to imagine building a ++nest for finite type nouns. (The problem is not even equivalent to SAT, because there is a unification stem but no intersection stem.)

But for (logically) infinite types? Yes - actually, the problem is straightforward. But the solution requires us to use %hold types as search keys.

Essentially, ++nest can begin by assuming that every ref is a sut, then traverse the parallel trees searching for any case of a ref that might conceal a non-sut. In this traverse, we can simply keep a set of the [sut ref] problems we are solving:

+ gil=*(set ,[p=type q=type])

Again, gil is just the ++nest stack as a live problem set.

If we descend into another instance of the search tree we're actually in, ie, currently searching for exceptions to the compatibility assumption, there is no reason to restart our search. So, we can prune and ignore these recurrences. And so, we can write a decent ++nest. " -- http://doc.urbit.org/doc/hoon/tut/6/

the author of Hoon, then, prefers explicit to implicit laziness. But couldn't we have both? Just like symbolic links in Unix can be implicitly followed, or can be explicitly treated as files.

This is another application example for Oot levels. At a higher level, you might see a list as infinite. At a lower level, you might see the generators (%hold's).

---

another example might be towers of Maybes ? or perhaps nullable types vs. maybes?

---

natural language constants for kythe things like alias and defines and annotates-with-metadata, but also ootcore things like forall, conditional. note that some oot core things seem to do double duty as imperative control and logical assertions, eg forall/foreach, if. is Kythe annotateswithmetadata different from transactions b/c that is content, not meta? i think so. distinguishing 'content' and 'meta' annotations is another poteetial way of having 'levels'.

---

muKanren has 4 core operators [1]:

miniKanren has 4 core operators [2]:

'fresh' and 'call/fresh' are analogous to 'let' (or 'lambda' in python or lambda calculus). 'disj' is analogous to 'or', and 'conj' is analogous to 'and'. 'conde' is analogous to 'cond' (in Scheme, or 'if' elsewhere), and 'run' is analogous to 'eval'.

in Oot we'd want to just use let, or, and, if, eval, instead of introducing new, analogous words for each DSL. Presumably in some or all implementations, the implementations of the muKanren and miniKanrel DSLs depend on defining these as new functions, which is why new names are used. I would, however, prefer to just reuse the existing analogous terms from the base language, and disambiguate which one is being called by context. This 'context' could be the 'levels' that i am searching for for Oot.

Note that sometimes you might have an expression that needs to mix, eg, 'or' and 'disj' in a single expression (where 'or' is from the base language, and 'disj' is from muKanren). So some sort of 'quoting' or namespacing needs to be used to allow this (eg base::or vs mukanren::or).

If this 'namespacing' convention is used, then of course there should be a way to set the 'default namespace' for any given lexical scope (eg:

mynamespace::

y = a or b

could be short for:

y = a mynamespace::or b

)

but we also need some way for namespace changes to be inferred, eg if you have a variable containing a muKanren goal expression, then when operating on the value of this variable, 'or' should by default mean 'disj' (which is equal to mukanren::or).

This is all very similar or identical to ad-hoc polymorphism.

---

See the AST data model in [[oot-ootAssemblyNotes7?]]. Since some of the AST stuff is just graph stuff at a higher 'level', can we combine them? eg combine BASE and VAL, make CHILD a shortcut for EDGE in some way, combine META and LABEL?

---

in fact, maybe which implementation of an interface is chosen could be a function not only of the interface, but also of a 'context', which is akin the idea of a 'level' metaprogrammatically changing the meaning of a set of symbols.

---

some related thinking is in proj-oot-ootAssemblyNotes11.