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

[mbacarella]

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

[hyphenrf]

Sort-of: xvw/ppx_measure

[yawaramin]

FWIW, @xvw has (IIRC) said that that PPX should not be considered production-ready.

[octachron]

It is possible to emulate this feature with enough phantom types and some axiom functions. But at some point, you will blow up your complexity budget.

[dimitris]

From a quick look at this document (link below) it seems that some extension would be needed in the type system, including unification.

http://typesatwork.imm.dtu.dk/material/TaW_Paper_TypesAtWork_Kennedy.pdf

[xvw]

To be very honest, it was mainly an excuse to learn how to use/write PPX. I don’t have the intuition that the tool is usable … and it’s far more limited than what FSharp offers. (For example, you can only multiply a “unit” by an integer, because I can’t stand the m(x) * m(y) = m2(x * y)).

[XVilka]

The chances that flight software not on ground segment will run F# are zero though, at least with modern technology.

[EduardoRFS]

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

[kantian]

You don’t need GADT magic to encode system F, OCaml with its module system is more or less system Fomega. The fun keyword is the lambda and the functor keyword is the big lambda.