Re: A Plan for Hacking

[Ludovic Courtès]

Hi Noah,

>>>   - 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 was referring to the ability to connect code snippets at run-time (by
means of use-modules, C-x C-e in Geiser, etc.) and have an evolving,
live system.

Having types associated with values makes this easier.  It may become
harder once the compiler has built assumptions into the generated code
about the types each procedure expects.

[...]

>> 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.

Yes, that would be good too.

>> 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.)

About Kanren, there’s “The Reasoned Schemer”.

About Coq, I’ve heard that the Coq’Art, by Bertot & Castéran [0] is a
nice read, but it’s heavy.  ;-)

[0] http://www.labri.fr/perso/casteran/CoqArt/index.html

>> 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.

Oh, right.

Thanks,
Ludo’.