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/