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 Jasper 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?

---