luqui

I find myself wanting an image-based functional environment, like a persistent ghci. I want to use it to track my TODO list, do quick one-off computations, store miscellaneous data and analyze it. Basically it's an environment where I can store my stuff that has the power of a Turing complete functional language. Like spencertipping's self-modifying perl scripts, but functional instead.

I'd also like to design it well. It's kind of a hacky purpose, but I might as well put some thought into its design and apply some of my recent ideas about modularity. In such an environment everything is constantly changing, and yet it ought to be purely functional, because pure functions are cool. So the module system has to be able to handle such a dynamic environment -- reusing old code in new contexts.

In an interactive environment, we are not usually designing for modularity. Instead we just enter expressions, save values away, inspect them, and enter more expressions. I would like to reuse any value I have give

luqui

Ok so I keep having the same idea over and over again. Maybe that means I like it.

This time I'm phrasing it like this: combining spencertipping's perl objects with functional ideals and distributed references a la Udon. These objects can have computational content (like perl objects, unlike Udon) and are defined in terms of an explicit abstract basis (unlike both).

Having tried to write this several times, I really want to be minimal about it. Not minimal as in perfect and beautiful -- minimal as in a small amount of work. I can give it water and sunlight later.

But first, as with all my recent projects, I have to determine what I mean by an abstract basis. I'm beginning to believe the idea is not reliant upon, but connected to the idea of types. A basis without types is just made of names, which are sufficiently ambiguous that they cannot be methodically searched or computationally combined (nor is their usage clear without examining their definition). Types allow the computer to see what is going

luqui

Our task is to characterize a relationship between an abstract syntax tree and concrete syntax, much like the development in [Invertible Syntax Descriptions by Tillmann and Ostermann][1]. We have an additional constraint, however. We aim to make the mapping interactively editable -- that is, convert editing commands on the text to transformations on the abstract syntax.

For example, consider a simple arithmetic grammar with precedence. Given this abstract syntax tree (in S-expression notation):

(plus 3 4)

which is pretty-printed this way:

3 + 4

luqui

In this document I attempt to build some intuition for the ordinals by constructing several concrete well-orderings of the naturals with order types up to (and including!) epsilon 0.

Ordinals are all about well-orderings. A well ordering of the naturals is an ordering -- call it <~ -- on the naturals that has no infinitely descending chains. So the reverse ordering, x <~ y iff y < x, is obviously not a well-ordering because it has the infinitely descending chain 1 ~> 2 ~> 3 ~> ....

However, the usual ordering is a well-ordering, because if you start at n, you only get at most n steps before you have to hit 0. The usual ordering is called "omega", which I denote w.

luqui

Let [ ] : Ord -> Relation Nat be a function that realizes an ordinal into a well-ordering of the naturals with that order type.

Given a relation R on the naturals, we define the restricted relation R(<n) to be R but just acting on the first n naturals.

Defn: [ ] is continuous iff for every series of ordinals a_i whose limit is l, for every natural n, there exists an i such that for all j > i, [a_i](<n) = [l](<n).

Intuitively, if you are only looking at a finite prefix of the naturals, you can get to a limit ordinal by going finitely high up its limit sequence.

luqui

sq = floor . sqrt . fromIntegral

primes = 2:filter (\n -> all (\m -> not (m `divides` n)) (cand n)) [3..]
    where cand n = takeWhile (<= sq n) primes

m `divides` n = n `mod` m == 0

fibs = 0:1:zipWith (+) fibs (tail fibs)

l5 p | p5 == 1 || p5 == 4 = 1

luqui

mergeEq :: (a -> a -> Ordering) -> [a] -> [a] -> [(a,a)]
mergeEq cmp (x:xs) (y:ys) =
    case cmp x y of
        EQ -> (x,y) : mergeEq cmp xs ys
        LT -> mergeEq cmp xs (y:ys)
        GT -> mergeEq cmp (x:xs) ys
mergeEq f _ _ = []

luqui

Daniel Spiewak's [proof][1] that there exist total functions which are not inductive uses the following assumption:

I am going to assume that the problem of determining whether some arbitrary function is inductive [...] is in fact decidable. I actually don't have a reference on this one, but it seems like a fairly reasonable assumption. Formally:

exists D, forall f, f in I <=> (D(f) = TRUE)

I have modified the statement of the assumption slightly. In fact, my modification is not equivalent to the original, since my version says "there is a decider for inductive functions" where the original is "there is a single decider for both inductive and coinductive functions". It is conceivable that there is only a technique that can tell whether a function was either inductive or coinductive but can't tell which it is, in which case the above statement would not be implied. But that is an exotic enough possibility that I'm comfortable with my simplification.

However, the statement of the assumption

luqui

Maybe if I keep rewriting this document I will eventually stumble on what I want.

Goals:

1. Support for programming environment with ever-increasing social vocabulary (i.e. 'helper' functions become global vocab words).
2. "Type system" whose primary purpose is to document the meanings/usages of words.

The way I have been picturing (2) is by allowing types to be fabricated into existence without a formal (or representational) definition. For example, if we wanted to talk about primes as a type, we could, but we wouldn't have to describe to the computer what it means to be prime. It is human communication. So:

-- inverse p n finds the multiplicative inverse of n mod p.

luqui

Going a bit crazy here... I want to make some language-design art, but I can't decide on what to do.
There's propdoc, interactive coding environment (ice?), new ideas floating around wrt syntax and focus. I just want to do something!

Ok, more thinking then, there needs to be a focus to the excitement, and I can't make a good ice without a type system, and existing type systems are too intensional for it. Auto-abstraction might be too lofty a goal, that could be what is constraining me. And yet, it is sortof essential to the idea. Well, there is really only one problem with it, and that is the lexicon distinction I have been talking about. But that is a modularity problem; module systems need to be the most perfect, they are the outermost part of your code, they almost touch the cold outside air.