search

JacquesCarette / Drasil

Generate all the things (focusing on research software)
https://jacquescarette.github.io/Drasil
BSD 2-Clause "Simplified" License
143 stars 26 forks source link

Typing Rules #2946

Closed balacij closed 1 year ago

balacij commented 2 years ago

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.

JacquesCarette commented 2 years ago

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

balacij commented 2 years ago

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

JacquesCarette commented 2 years ago

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.

balacij commented 2 years ago

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.

balacij commented 1 year ago

Re-writing them now.

balacij commented 1 year ago

I will send them over along with the rest of Chapter 7.