This seems like a pretty nice way to protect against the NASA Mars Climate Orbiter unit mixup literal crash. https://docs.microsoft.com/en-us/archive/blogs/andrewkennedy/units-of-measure-in-f-part-one-introducing-units

Is there a way to do this kind of F# refinement typing in OCaml?

EduardoRFS March 24, 2021, 9:12am 8

I wonder if we can encode full System F(no inference) with enough GADT magic.

1 Like

Topic		Replies	Views
Resources for building a Polymorphic Lambda Calculus compiler? Learning	6	1480	March 9, 2021
Update on the big ppx refactoring project Community ppx	6	2093	September 30, 2019
How can you "un-functorize" an API to make it polymorphic while retaining type safety and efficiency? Learning package-design , polymorphism , pattern	10	286	January 23, 2025
GADTs, phantom variables and type aliases Learning gadt	4	816	August 19, 2020
Type system and polymorphic let's Learning	1	226	July 18, 2024