Home » forums » LtU Forum

Typesetting a Type System with Color-Coding

I've recently been working on formalizing the type system for one of my programming languages. While writing out the rules for inference I found it helpful to use both traditional type syntactic inference as well as some categorical language. The back-and-forth is so common that I have considered color-coding terms to indicate when they correspond to an object or morphism in which category.

My question for LtU is whether color-coding seems goofy or maybe helpful in some contexts. I have considered alternatives and I think there are three options:

1) Color-code terms by Category
2) Add text describing which terms correspond to which Category
3) Alter the term/type syntax to make category an explicit syntactic property

By andrew johnson at 2023-08-05 16:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 883 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Syntax highlighting is so

Syntax highlighting is so common in source code now that it is rare to find anyone that does not use it. Colour is a useful way to add annotations to parts of text as we process it so well as contextual markers. It is less common in equations but there is some work that shows it can be useful. I've seen some uses in teaching maths, and it seems to work well for physics. Here is one example, https://betterexplained.com/articles/colorized-math-equations/

This is one case where a picture speaks a thousand words, posting a link to examples of your highlighting would help people to give feedback.

By Andrew Moss at Mon, 2023-08-07 07:05 | login or register to post comments

Color and Text

I like the idea of colored equations + colored text. It says more with less effort. Thanks for the example.

By andrew johnson at Tue, 2023-08-08 00:41 | login or register to post comments