Archive for February, 2007

Progress at last

This afternoon, I finally managed to get InforML to acceptably process one of my key examples. You start by defining some abstract data type

# Simple module defining an abstract datatype for rational numbers

module rational : sig
label Rat

type rat : (Lab -> * @ Rat) @

fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @

# Approximates to the nearest integer
fun toInt : ((rat @ ) -()-> (Int @ )) @

end = mod

newlabel Rat

type rat : (Lab -> * @ Rat) @ = (fn l:Lab => (Int @ l, Int @ l) end)

fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @
fun fromInt 〈l:Lab〉 (i : Int @ l) : rat @ l = (i, 1)

# Notice this is a more general type than the one
# exposed by the signature
fun toInt : 〈l:Lab〉 ((rat @ l) -(l)-> (Int @ l)) @
fun toInt 〈l:Lab〉 ((i1, i2) : rat @ l) : Int @ l = i1 div i2

end

The important thing to note here is that the abstraction assumes the invariant that the second integer in the pair will never become zero. Next you define a malicious function using type analysis

fun badtcase : 〈l:Lab (a:* @ l)〉 l <: info a => (a -(l)-> a) @
fun badtcase 〈p:Lab (b:* @ p)〉 (x:b) : b =
typecase b
of (Int @ p, Int @ p) => (1,0)
| _ => (x : b)
end

Now you use your malicious function to create an invalid instance of the abstract data type

val x = badtcase (rational.fromInt 42);
val x : (rational.rat @ rational.Rat)

And finally notice that this new corrupted value of the abstract data type cannot be used to cause a divide by zero, as

val _ = rational.toInt x

has an information content of rational.Rat which is greater than as specified by the signature.

Yes, I know that WordPress obliterated my whitespace, but I don't really feel like trying to fix it by hand at the moment. It also seems to enjoy converting all my <div> tags into <p> tags.

Comments

Extreme latency

I've been feeling kind of guilty about not writing much recently.  Mostly it is because lately all my time has either been devoted to working on the implementation of InforML or trying my best not to think about InforML.

Anyway, my latest debugging run just finished, so I should get back to deciphering the results.

Comments

Infested

I managed to resolve the bind I had found myself in yesterday, but switching from reuse via polymorphism to reuse via state change. This was not too painful as the function in question was already pretty stateful. So instead I just have the caller do final bit of computation and clean-up.

However, I then spent nearly the entirety of the afternoon chasing after a bug, that I now strongly believe has more to do some fundamental assumptions I made when I designed the constraint system versus sloppy coding or some such. Hopefully I'll figure something out tomorrow.

At this point I am less likely to rewrite major portions of the InforML code base in another language, though I am seriously thinking about implementing the core language type checker and evaluator in Coq or Scala. Though I am somewhat skeptical as to whether my schedule will allow me to really take advantage of the expressiveness allowed by Coq's type system, or whether it will just get in the way.

I'm also seriously considering taking a few days this week to just focus on making the current InforML codebase easier to debug and maintain. On one-hand, this code will never be used as anything more than a prototype for experimentation (unless I were to use it to write a bootstraping compiler in some unknown future) so I don't want to spend too much time on things that will just be thrown away before too long. However, if it can save me from another afternoon of debugging like today, maybe it would be worth it.

Comments

Coding yourself into a corner

It is on days like this that I can empathize with people who are are wary of the restrictions that static typing can place on them. In particular I've kind of coded myself into a corner in the development of InforML where I need: use polymorphic recursion (which Standard ML does not provide), duplicate a nontrivial amount of code at least half a dozen times, or attempt to manually manage the recursion myself. I just spent several hours on the third approach. I think it may still be possible yet, but I'll need to go back an revise just all the code I had just changed to use thunks as well.

It is almost to the point that I'm seriously considering rewriting a large portion of InforML in Haskell or Scala. I would probably keep the parser, by making it output XML or s-expressions that can be easily parsed back into an AST. But this would mean I would get proper support for monads, and the ability to write a number of things in a type-directed fashion, cutting out huge amounts of boilerplate.

However, it may be just more practical to duplicate the code that is causing the problem and hope I don't need to revise it that much more. Anyway, I am going to take a break for at least a few hours before moving forward. It is just so frustrating that I have to waste time on this sort of stuff when I have plenty of other »real« technical problems to be solving, instead of having to make up for the fact that Standard ML is antiquated.

Comments (1)