I quit on the Hi Language and eventually developed an interpreter for the Egel Language. I lost some of the code of Hi but intend to reuse some of it now (several abstractions like state machines, 'monadic' operators, and functional maps.)
Monday, October 25, 2021
Friday, October 16, 2015
Goodbye Hi. Last Post.
So I gave up on implementing a typed language. The problem, in a nutshell, is that I couldn't convince myself I could solve a particular problem associated with constraint typing.
The problem: In order to prove a specific goal you need all information derivable from a term; and with juggling around only local information, I cannot convince myself I could arrive at a typing system which would prove specific goals given all information derivable in the term.
I am not sure how general this problem actually is. The closest typing system I could look at is Haskell, and there are no results on this problem. I gather they patched a system together which usually works.
The language I am now developing looks naked though. It'll become an experiment in how to write untyped algebraic specifications.
Too slow for anything useful probably but a nice experiment.
The problem: In order to prove a specific goal you need all information derivable from a term; and with juggling around only local information, I cannot convince myself I could arrive at a typing system which would prove specific goals given all information derivable in the term.
I am not sure how general this problem actually is. The closest typing system I could look at is Haskell, and there are no results on this problem. I gather they patched a system together which usually works.
The language I am now developing looks naked though. It'll become an experiment in how to write untyped algebraic specifications.
Too slow for anything useful probably but a nice experiment.
After the new language is developed enough, I'll start a new blog. Goodbye Hi.
Tuesday, September 29, 2015
Hi Relegated
I concede. The minor typing systems I could come up with didn't handle all corner cases well. Instead of thinking about it more, I decided to start on a new untyped language.
Wednesday, June 24, 2015
Algorithm W
I like the prover in my bootstrap but, yeah, there's algorithm W too. So, I decided to go for that. Gone are the bisimulation proofs of type equivalences but I simply don't know what I am dropping there and can't care to figure it out. At least with W I know it has been proven correct, terminates, and gives reasonable performance on small terms.
Which also implies that I'll need to figure out how to do constraint checking with W. But, in some sense, W already checks constraints by providing a proof, a most general unifier, for types.
So. How hard can it be? Right...
Which also implies that I'll need to figure out how to do constraint checking with W. But, in some sense, W already checks constraints by providing a proof, a most general unifier, for types.
So. How hard can it be? Right...
Sunday, June 21, 2015
Log 062115
Made a few small changes to the AST. Implementing a number of routines ahead of time until I figure out what to do with the type checker.
The type checker, as implemented in the bootstrap, is okay-ish. Not too shabby. The major difference between it and other functional type checker is that it records substitutions as type equivalences. I probably could speed it up already by factoring out different propositions. Moreover, I decided against using the gathered type equivalences to attribute the tree; I could do without recording substitutions.
Still, there's this thing about being able to typecheck cyclic types. Suppose, you have a type definition which unravels to the following:
t
/ \
/\
t
/ \
/\
.. ..
The type checker I now have "records" substitutions. It should therefore be able to prove type equivalences like the above by stating an equivalence, unfolding the type once, and using the postulated type. (Conceptually, the second "t" in the picture above becomes a cycle pointing to the first "t'.)
But that doesn't seem to be a problem in practice. To prove equivalences ML compilers simply unravel types a few times and use the definition to "close the cycle".
Ah well. First kindification I guess.
The type checker, as implemented in the bootstrap, is okay-ish. Not too shabby. The major difference between it and other functional type checker is that it records substitutions as type equivalences. I probably could speed it up already by factoring out different propositions. Moreover, I decided against using the gathered type equivalences to attribute the tree; I could do without recording substitutions.
Still, there's this thing about being able to typecheck cyclic types. Suppose, you have a type definition which unravels to the following:
t
/ \
/\
t
/ \
/\
.. ..
The type checker I now have "records" substitutions. It should therefore be able to prove type equivalences like the above by stating an equivalence, unfolding the type once, and using the postulated type. (Conceptually, the second "t" in the picture above becomes a cycle pointing to the first "t'.)
But that doesn't seem to be a problem in practice. To prove equivalences ML compilers simply unravel types a few times and use the definition to "close the cycle".
Ah well. First kindification I guess.
Thursday, June 18, 2015
A Small Derivation
I completely forgot what my prover does; I rushed it anyway. So, I worked out a rough example by hand below to get some grasp on it. In a bottom up fashion it collects a mess of constraints, say it gathered
So, okay. Guess that works. I made a reasonable estimate of how constraints should be solved, dump the mess in the prover, from the antecedent I read off how to attribute the tree with the solved constraints.
It doesn't seem to handle intermediaries well, though. Guess I need to check it with the algorithm. (Hmm. Intermediaries should remain on the left-hand side of the equation?)
int:*∧ (::Ord int) ⊢t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)
It then proves that (roughly) likes this
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧
k0 = ka =* ∧ t0: = int:*∧ k1 = kb=* ∧ t1:* = int:*
⊢
-----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧
k0 = ka =* ∧ t0:* = int:*∧ k1= kb = * ∧ t1:* = int:*
⊢ (::Ord int)
----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ t1:k1 = t4:k4
∧ k0 = ka =* ∧ t0:* = int:*
⊢ t1:k1:* = int:kb ∧ (::Ord t1)
-----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4
⊢ t0:k0 = int:ka ∧ t1:k1 = int:kb ∧ (::Ord t1)
----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4
⊢ t0:k0->t1:k1 = int:ka->int:kb ∧ (::Ord t1)
---------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 ∧ t0:k0= t3:k3
⊢ t1:k1 = t4:k4 ∧ t0:k0->t4:k4 = int:ka->int:kb ∧ (::Ord t1)
-----------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4
⊢ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 ∧ t3:k3->t4:k4 = int:ka->int:kb ∧ (::Ord t1)
----------------------------------------------------
int:*∧ (::Ord int) ⊢ t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)
It doesn't seem to handle intermediaries well, though. Guess I need to check it with the algorithm. (Hmm. Intermediaries should remain on the left-hand side of the equation?)
Log 061815 - B
Right. I started implementing a general prover, then after the first few lines of code, decided against it. Thing is, I have a prover which works on terms like this
It discharges each consequent given what it knows by inspecting the antecedents. Antecedents and consequents may be anything; e.g., kind equalities, type equalities, instantiation requests, etc. While proving a goal new consequents, sometimes an antecedent, may be introduced (trivially).
Thing is, I don't trust the time complexity of the algorithm. Checking for a consequent whether an antecedent exists is linear (times the term size of the antecedent), substitution is linear (times the term size), almost every step the prover takes is two of these linear, possibly quadratic, operations. As far as I know, proving in this general manner might be cubic.
So, I am working in the unknown here. Looks to me I want to keep the number of antecedents as far down as possible to keep the number of lookups and substitutions down, might also be that it is cubic but pragmatically that doesn't matter since you only operate on small numbers of small terms, lastly, since I sometimes am doing a 'bisimulation' proof, I might actually need to do it this way.
Stuck.
a0 ∧ ... ∧ an ⊢c0 ∧ ... ∧ cm
It discharges each consequent given what it knows by inspecting the antecedents. Antecedents and consequents may be anything; e.g., kind equalities, type equalities, instantiation requests, etc. While proving a goal new consequents, sometimes an antecedent, may be introduced (trivially).
Thing is, I don't trust the time complexity of the algorithm. Checking for a consequent whether an antecedent exists is linear (times the term size of the antecedent), substitution is linear (times the term size), almost every step the prover takes is two of these linear, possibly quadratic, operations. As far as I know, proving in this general manner might be cubic.
So, I am working in the unknown here. Looks to me I want to keep the number of antecedents as far down as possible to keep the number of lookups and substitutions down, might also be that it is cubic but pragmatically that doesn't matter since you only operate on small numbers of small terms, lastly, since I sometimes am doing a 'bisimulation' proof, I might actually need to do it this way.
Stuck.
Subscribe to:
Posts (Atom)