Coding 2025-05-19
Okay, I got the simply-typed lambda calculus code up to snuff in terms of coverage and mutation coverage. Unfortunately, I'm not ready to elaborate up to System F, because I'm not totally sure how I'd like to.
See, the issue is that the elaborations, at least to start with, have lots of similar structure, just with More Stuff, and the way to fit the More Stuff in is... I think I see how I want to do it, but there are some complications to address. Because suddenly it's possible to give expressions new kinds of types, and have new kinds of expression. So, how to accommodate these extensions? It sure seems like the way forward is to parameterize the types and expressions that are allowed, which may push Mypy's support for recursive type expressions to the limit. Something like:
- type Type[T] = BaseType | FuncType[T] | T
- type Expression[T, E] = Value[T, E] | Abstraction[T, E] | Application[T, E] | E
- type STLCType = Type[Union[()]]
- type STLCExpression = Expression[Union[()], Constant[Union[()], STLCExpression] | Operation[Union[()], STLCExpression]]
- or maybe type STLCExpression[T, E] = Expression[T, Constant[T, STLCExpression[T, E]] | Operation[T, STLCExpression[T, E]]]
I'll have to think about this and experiment with it a bit. Hopefully at a time when the internet isn't going up and down like a yoyo.
Anyway, that's more than enough time writing, so let's wrap this up.
Good night.