entry
Syntax-Directed Translation and Type Theory
A week has passed since I created this post, and I have to say that I kind of enjoy waiting for the weekend to arrive so I can write about my progress and all the things I learned.
As I said in my first post, it’s my first time writing any kind of public notes or
thoughts to anyone who is not myself, and it’s a weird feeling, but in a nice way.
The things I learned this week
This week has been a bit tough, mainly because I had to prepare for an exam I have next week and I didn’t have a lot of time to learn a lot of things, but I did learn some little nuggets!.
Some of the things I learned this week are Syntax-Directed Translation, λ-calculus & Type Theory.
Syntax-directed Translation
This semester I’m taking a class related to Compilers, where we learn about the first phase of compiling(analysis phase) and
we learned about how you can check if the source file is semantically correct using attribute grammars.
In particular, we learned about Syntax-Directed Translation, or in shorthand SDT.
Usually, you have a Context-Free Grammar for analyzing the syntax of your language, but for semantic analysis you need more information and context. You can’t represent every single aspect of you language only using a CFG because of its restrictions.
That’s why we use an extended grammar called an attribute grammar. In particular, we use Syntax-Directed Translation. This type of grammar has special annotations on the right-hand side of the productions, providing context and meaning, and checking validity while parsing the source file.
The main idea is to check the semantic meaning while you parse the file and create the Abstract Syntax Tree (AST).
In reality, it doesn’t have to be an AST; it can be any type of Intermediate Representation(IR).
This grammar works on top of the grammar you had for the parser.
The SDT has two main parts:
- Attributes: which defines properties for grammar symbols. It can be a type, a value, a position,..
- Semantic actions: this actions define how attributes are passed around the AST and how attributes are assigned to other grammar symbols.
Basically you have 2 types of attributes(synthesized & inherited) depending on the flow direction.
Example
For demostration purposes I will show an example on how the syntax looks like:
Given this grammar:
E → E + T
E → T
T → digit
The corresponding SDT would look like this:
E → E1 + T { E.type:= E1.type if E1.type==T.type }
E → T { E.type := T.type }
T → digit { T.val := digit.type }
In this example, we only have synthesized attributes. These attributes always flow upwards the parse tree. We are checking the types of each rule.
In the first rule, the type of E1 + T should be the same(depending if the language accepts coercion) and it will be assigned to E. In the next 2 rules, we just assign the type to the left hand side.
This is not an academic book!
I don’t want to get too much into the theory, mainly because this blog is not meant as a learning resource, rather a projection of my mind and my thoughts.
I really find the SDT quite amazing, how you can check the validity(semantically speaking) of a source file just by embedding some annotations around your parse grammar.
If the subject really interests me, I usually try to expand my knowledge by doing some research and watching some YouTube videos about it, or reading some papers.
In the process I discovered new things like type coercion, which is useful when you have an expression with two similar types and have to decide the final type(e.g.,integer with float), optimization techniques, type inference, etc.
I also discovered a new field called Type theory, in hand with λ-calculus and got astonished.
Type theory & λ-calculus
I first heard about λ-calculus when I was researching about how you can archieve type inference, and everything I found talked about λ-calculus and some random theory about types…
So I decided to investigate about it, with some simple explanations online and videos.
This was my honest reaction
WHAT I’M EVEN LOOKING AT
At first glance I didn’t understand ANYTHING, like literally anything. What are they talking about?, what’s that weird looking syntax, do I need a PhD to understand the basics?.
This is an example of what every video looked like:
I was really overwhelmed with that sudden slap of reality check. I realize there is a whole mathematical world around Type systems and type inference, and knew that It will not be an easy journey.
With some time, I started getting some words, definitions, what the syntax meant…
I ended up looking type-theory videos(which I don’t fully understand yet, but is something) and tried reading some papers around the subject.
Relax, you just need time
At the end of the week I ended up knowing the basics of λ-calculus and how type-system’s work.
I feel like I entered the Functional Programming Cult’s space.
Even if I felt overstimulated about all the new things I didn’t knew I’m happy because I realized all the things I have yet to learn and all the opportunities to become better at this amazing field.
I have to realize that I can’t know everything, and if I want to, I will have to be patient and consistent. Nobody was born knowing everything.
Learn to love the journey, not the destination
I hope in the future I truly understand all this math-based systems and become a talented Compiler-engineer.
I will try to grasp more information on these subjects and dive deeper on SDT to get a better foundation on attribute-grammars.
Well, this is all I have to say this week. I don’t know if I will post weekly or when I feel like it. We’ll see :p
Thanks for reading and have a nice day!
other entries
- Syntax-Directed Translation and Type Theory2025-11-29
- The creation of my blog2025-11-23