Unfortunately, Refinement Types as all other types are only useful as long as you write them and prove (explicitly or implicitly) your code respect them. That's not the case for external code in libraries and frameworks, in your case for OCaml and JS code you have to interface with. You can declaratively ascribe (`assume`) types to external functions but you have no guarantees these functions obey to ascribed types especially when you update your dependencies. And even then you're very likely to suffer from information loss due to underspecification of external types, especially when your data or functions get passed through external functions and back. Even built-in `map` function in F* looses type information about function and data given to it.
So overall your code is going to be only as good as OCaml/ReasonML types. Basically on par with F#. That's why it makes little sense to automatically convert OCaml to F* - you're not going to get the most important part, more precise Refinement Types as OCaml types lack them and you're unlikely to recover much even fully analyzing the source code. At least that's what my very limited experience tells me. :) Best regards, *Alexander Tchitchigin* Software Developer *Positive Technologies* Tel.: +7 (495) 744-01-44 Fax: +7 (495) 744-01-87 E-mail: achichi...@ptsecurity.com www.ptsecurity.com On Fri, Dec 7, 2018 at 4:18 PM Joel Jacobson <j...@compiler.org> wrote: > On Fri, Dec 7, 2018, at 5:03 AM, Alexander Tchitchigin wrote: > > Hi Joel, > > As long as your main interest is Web development, have you considered F*'s > "father" - F# (https://fsharp.org)? > In particular, WebSharper (http://websharper.com/) and Fable ( > http://fable.io/)? > > > On the other hand, maybe the problem with polymorphic comparisons in OCaml > might be solved with Modules and Functors? > > > Yes, I've looked at F#, but I really want to use F*, it has many cool > concepts that I want to benefit from, such as inferred type-and-effects and > the use of Z3 to prove things about your code. I'm curious to know if there > are any plans to help developers semi-automatically convert code fragments > from OCaml to F*? > >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
