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.
With regards to my graphical dependent type idea, I have been having some new thoughts. In that system, you have "tangible" objects representing data and knowledge. That is what I want for propdoc, but I want it less unified and less formal than DT languages, because knowledge manipulation is somewhat annoying in those languages (eg. projecting sigma types). But the key idea should still be there: knowledge is data.
The knowledge system should be soft; hand-coded admitted inferences should be allowed with documentation. E.g. if p is even and prime then I know it is two, so if I say that the computer will simply believe me. This should be common practice, so as not to put too much emphasis on the possibility of perfect formal proof. Maybe the knowledge system should be sufficiently limited so that perfect proofs are not possible, just to drive the idea home.
Knowledge could be represented by Prolog-style predicates. With the right kind of solver, we could encode types as predicates, and the engine would reduce to HM inference. I think that is the most realistic ambitious goal, and would really give the system elegance.
-- hastype(X Y, T) :- hastype(X, A -> T), hastype(Y, A).
-- hastype(\X. Y, A -> B) :- hastype(X, A) => hastype(Y, B).
(+) :: Int -> Int -> Int
-- this is a proposition. Read it as hastype((+), int -> int -> int).
map :: (a -> b) -> [a] -> [b]
-- hastype(map, (A -> B) -> list(A) -> list(B)).
1 :: Int
-- hastype(1, int).
foo x xs = map (x +) xs
--
|- hastype(\x. \y. map (x +) xs, T)
T = A -> B
hastype(x, A) |- hastype(\y. (x +) xs, B)
...
And so on, solving like a good ol' logic language. We need to be able to handle variables like in the lambda typing rule. Perhaps lambda is how we do that: we can match against a lambda. Does the HOU problem appear? Anyway, we will treat terms as their syntax for the purpose of the logic language, so we don't run into Rice.