JacquesCarette
Typing Rules
I'm currently working on defining the typing rules of the expression language (and related things).
I've created a stub file from my main thesis that contains just the typing rules.
I will continue to work on it, but I figured this is a good point for feedback.
Thank you.
I think we need more precision about what the typing rules mean. For example, we should start with a grammar for the types themselves.
There's also some difficulties. For example, for "Real numbers", the top "d : Double" is a judgement about a Haskell thing (d) and a Haskell type (Double) while the conclusion seems to be about something else, in a grammar that I'm not certain about. Also, is Literal really a type? Real?
I think it would be good to "step away" from the low-level details, and have some sort of abstract grammar for our term language and our type language. Then we can see if our current encoding of the language in Haskell can support a type system.
For sure, rule (51), i.e. 1.3.3 for Symbols, is problematic: x appear in the type, but there is no way to tie it to C[u].
That sounds like a good plan. I will write out the grammar right now.
Regarding the difficulties, I can see what you mean -- it is too close to Haskell, and I will try to step away from the low-level details as you mention.
Regarding Literal, yes, it does exist. Regarding Real, it's currently a variant of Space (I somewhat use it interchangeably with Double, but, like you said, I think it's because it's too low-level oriented).
Regarding symbols, I agree. In part, this is why I've been trying to add a type parameter for QuantityDicts. Similar problems would occur anywhere that has the untyped symbols (QuantityDicts).
Part of the point of doing this is to really pinpoint where the problems are. And perhaps get an advanced peek at problems we hadn't yet spotted.
Okay, I've posted an idealized version of the existing syntax in approximately the same style as the "Practical Foundations for Programming Langauges" book.
EDIT: Unfortunately, the link is a 404 now but the rules still live inside of my thesis, in Chapter 5.