Re: A Plan for Hacking

[Noah Lavine]

Hello,

>>   - You write a function that assumes its arguments are of a certain
>> type. You'd like to be sure this is true, so your program won't throw
>> exceptions in the middle.
>
> That would be cool.  However, I suspect that for best results you’d want
> procedures to have type annotations, as in Racket’s Typed Scheme and
> Bigloo; otherwise it may be impossible to determine type info most of
> the time—e.g., a public top-level procedure used in another module.
>
> (It’s not clear to me whether this can be done without seriously
> compromising on dynamic module composition.)

I think it can be done effectively, but I'm not quite sure what you
mean by "dynamic module composition." Do you mean that this might
prevent you from making modules that use arbitrary other modules? Or
that it might not work if you loaded modules at runtime from the REPL?

I agree that we'll want type annotation. But you can also think of
type annotation as a special case of the more general idea of caching
intermediate steps to speed up analysis. After all, in theory you
could always rederive the type information for each function from its
source code every time you needed it. I wonder if this is the only
case of caching that will matter, or if it is worthwhile to just make
a more general caching mechanism.

>> [...]
>
> These three items seem “off-topic” and less important to me.

Okay. I'm not sure what I think about them right now, because I am
very intrigued by the idea of using the analyzer to help correctness,
but you might be right. I will think about it more.

I thought of another use-case, and I wonder if you think this is
on-topic or not:

 - You write a parallel version of map that is fast, but only correct
if its argument has no side-effects. You'd like to use this parallel
map instead of the regular one, but only when it is correct.

> To reduce frustration, I would narrow the use cases a bit, or define
> short-term milestones.  For instance, you could decide to focus solely
> on type inference, or have type inference one of your major milestones.

Yes, type inference is a major thing. As I was thinking about a
compiler, the three things that seemed useful to me were type
inference, determining the outlines of big data structures that were
passed around (which could be type inference, depending on what your
type system is), and figuring out the lifetimes of heap-allocated
values.

> Kanren [0] and its companion book look like nice starting points to me.
> In particular, there’s a simple type inference engine written in Kanren
> that is actually usable with Guile 2.0 out of the box and could serve as
> a starting point.

Great! I will look at those. I have also found a book called Software
Foundations [0], which is an introduction to the Coq theorem prover.
It might be useful to be familiar with a few systems before starting
my own (or perhaps not even starting my own, but using Kanren). Do you
also happen to know of a book on formal logic systems in general, so I
can get more perspective? (I have one, but it doesn't cover as much as
I wish it did.)

I'm also interested in what Stefan Tampe is doing, because I believe
he's implementing a formal logic system in Guile. Stefan, does your
project connect to this one?

> And before that, make sure PEG actually gets merged.  ;-)

Yes, I will make sure that happens. Currently PEG is waiting on an
email about names. Once we agree on those, then I know of nothing
further blocking it from being merged.

Thanks,
Noah

[0] http://www.cis.upenn.edu/~bcpierce/sf/