3 ms·
You can hack up GADTs in F# - for example, https://github.com/Smaug123/WoofWare.Incremental/blob/9b8181ca1075102b1f62b06b82c8bb83c17f8f17/WoofWare.Incremental/T
by Smaug123 1y ago
You can hack up GADTs in F# - for example, https://github.com/Smaug123/WoofWare.Incremental/blob/9b8181ca1075102b1f62b06b82c8bb83c17f8f17/WoofWare.Incremental/Types.fs#L223 https://github.com/Smaug123/WoofWare.Incremental/blob/9b8181... (which uses https://github.com/G-Research/TypeEquality https://github.com/G-Research/TypeEquality ). (The other missing features I agree are missing.)
- nukifw 1y agoYes, the trick is expanded here: https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2008_Foundations_For_Structured_Programming_with_gadts.pdf https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2008_Founda... (if you have `Eq a b = Refl : a a eq` you should be able to encode every useful GADTs. But having a compiler support is nice for specifics reason like being able to "try" to detect unreachable cases in match branches for examples.
- debugnik 1y agoI've used equality witnesses in F# before, they kinda work but can't match proper GADTs. First you'll need identity conversion methods on the witness, because patterns can't introduce type equalities, then you'll realise you can't refute unreachable branches for the same reason, so you still need to use exceptions.