5 ms·

I actually wrote a bit about this on my website: https://azdavis.net/posts/lambda-cube/ https://azdavis.net/posts/lambda-cube/ I’ve been using my website as a

I actually wrote a bit about this on my website: https://azdavis.net/posts/lambda-cube/ https://azdavis.net/posts/lambda-cube/ I’ve been using my website as a way to practice writing, so please let me know what you think.

joshspankit 5y ago
No comments on the writing, but one thing to add: the syntax highlights for code get lost a bit. I would see them better either if they were a lighter black (aka dark grey), or had a different background than the rest of the text.
- bendbro 5y ago
  I second a higher contrast background/font color. Overall I like the minimal design. It might work to add some horizontal lines to break up sections
  - azdavis 5y ago
    Thanks! I updated it and replied to the parent comment.
- azdavis 5y ago
  Do you mean the inline code or code blocks? In any case, I tweaked the background to be more different from the page background (in both light and dark mode) and also gave inline code that same background. Does that help? https://github.com/azdavis/azdavis.net/commit/55199593abfb6eca9c0c9d542a224ae4cc81e2bd https://github.com/azdavis/azdavis.net/commit/55199593abfb6e...
  - joshspankit 5y ago
    Yep, works for me Thank you
wlib 5y ago
Very nice; you get to the practical lesson of it in a fairly straightforward manner while keeping interesting tangents where they aren’t distracting.
- azdavis 5y ago
  I really appreciate your feedback, thank you! > interesting tangents Yeah, I’ve found that explaining things by first giving an example and then generalizing often works better than trying to start with raw theory.
plafl 5y ago
I actually understood your article about the lambda cube much better. Also, very nice formatting and clean design, very readable on my phone.
- azdavis 5y ago
  Thank you! I’ve tried to make sure that my site reads well and loads fast, even on mobile. There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net https://github.com/azdavis/azdavis.net
AlexSW 5y ago
Nothing to add to the other comments, just wanted to add another data point that the website (on mobile) was perfectly clear and the information was all laid out and explained very well; I have no (constructive) criticism to give.
- azdavis 5y ago
  Thank you!
kinow 5y ago
Great post! I was going to share this one on the r/functionalprogramming subreddit when I found yours. A lot easier to read, and helps reading the Wikiversity afterwards. Thanks!
- azdavis 5y ago
  Wow thanks! Never had my stuff shared out before to my knowledge but I appreciate it! I’ll take a look :D
selestify 5y ago
Cool stuff! How do I decipher the symbols that make up the equations for "application" and "abstraction"?
- azdavis 5y ago
  The definition I gave at the end of the article (the thing starting with `t ::=`) is basically a context-free grammar describing the syntax for terms of the calculus of constructions. `t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`. The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.) So for instance, the case for application is: t(t') That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'. And the case for abstraction is λ(x:t) t' That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.
  - selestify 5y ago
    Awesome, thank you for the thorough explanation!
Icathian 5y ago
Really excellent explanation. I appreciate the writeup!
- azdavis 5y ago
  Thanks!

joshspankit 5y ago

No comments on the writing, but one thing to add: the syntax highlights for code get lost a bit. I would see them better either if they were a lighter black (aka dark grey), or had a different background than the rest of the text.

bendbro 5y ago
I second a higher contrast background/font color. Overall I like the minimal design. It might work to add some horizontal lines to break up sections
- azdavis 5y ago
  Thanks! I updated it and replied to the parent comment.
azdavis 5y ago
Do you mean the inline code or code blocks? In any case, I tweaked the background to be more different from the page background (in both light and dark mode) and also gave inline code that same background. Does that help? https://github.com/azdavis/azdavis.net/commit/55199593abfb6eca9c0c9d542a224ae4cc81e2bd https://github.com/azdavis/azdavis.net/commit/55199593abfb6e...
- joshspankit 5y ago
  Yep, works for me Thank you

wlib 5y ago

Very nice; you get to the practical lesson of it in a fairly straightforward manner while keeping interesting tangents where they aren’t distracting.

azdavis 5y ago
I really appreciate your feedback, thank you! > interesting tangents Yeah, I’ve found that explaining things by first giving an example and then generalizing often works better than trying to start with raw theory.

plafl 5y ago

I actually understood your article about the lambda cube much better. Also, very nice formatting and clean design, very readable on my phone.

azdavis 5y ago
Thank you! I’ve tried to make sure that my site reads well and loads fast, even on mobile. There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net https://github.com/azdavis/azdavis.net

AlexSW 5y ago

Nothing to add to the other comments, just wanted to add another data point that the website (on mobile) was perfectly clear and the information was all laid out and explained very well; I have no (constructive) criticism to give.

azdavis 5y ago
Thank you!

kinow 5y ago

Great post! I was going to share this one on the r/functionalprogramming subreddit when I found yours. A lot easier to read, and helps reading the Wikiversity afterwards. Thanks!

azdavis 5y ago
Wow thanks! Never had my stuff shared out before to my knowledge but I appreciate it! I’ll take a look :D

selestify 5y ago

Cool stuff! How do I decipher the symbols that make up the equations for "application" and "abstraction"?

azdavis 5y ago
The definition I gave at the end of the article (the thing starting with `t ::=`) is basically a context-free grammar describing the syntax for terms of the calculus of constructions. `t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`. The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.) So for instance, the case for application is: t(t') That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'. And the case for abstraction is λ(x:t) t' That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.
- selestify 5y ago
  Awesome, thank you for the thorough explanation!

Icathian 5y ago

Really excellent explanation. I appreciate the writeup!

azdavis 5y ago
Thanks!