search

marcoonroad / subtype-refinement

Refinement types encoded with private types in OCaml. :roll_eyes: :camel: :microscope: :books:
MIT License
10 stars 1 forks source link

How to use the program #5

Open Ayoya22 opened 4 years ago

Ayoya22 commented 4 years ago

Hello, I am new to Ocaml, please can you help me with simple instructions and concrete examples on how to run the program and also how I can use it to solve related problems. Thanks

marcoonroad commented 4 years ago

Hi Djoukam,

The intent and purpose of this library is to write enforced program invariants on type-level, but the proper validation is deferred to actual program execution/run-time. The only benefit of the usage of this library is when you and your team/coworkers use OCaml on the job codebase. Out of such context, this library is useless. I would recommend better tools for formal verification such as Coq, Idris or even property-based testing libraries such as QuickCheck (for Haskell) and Hypothesis (for Python). Of course, there are a bunch of property-based testing tools for other languages if your team uses another programming language.

Feel free to DM me if you need more guidance.

Ayoya22 commented 4 years ago

Hello Marco, Again thank you for your feedbacks they really help me a lot. Actually, I am working on a project wih the title "Applying Static and Dynamic refinement types" that is how I came across your project. They require me to explicitly work with the OCaml language but I am not very good at it. So I really want guidance towards that end. I want to present on it may be by the end of this week or next week so if I can have some guidance towards that end I will be very grateful. Thanks again Best regards Simplice.

On Mon, 11 Nov 2019 at 23:23, Marco Aurélio notifications@github.com wrote:

Hi Djoukam,

The intent and purpose of this library is to write enforced program invariants on type-level, but the proper validation is deferred to actual program execution/run-time. The only benefit of the usage of this library is when you and your(s) team/coworkers use OCaml on the job codebase. Out of such context, this library is useless. I would recommend better tools for formal verification such as Coq https://coq.inria.fr/, Idris https://www.idris-lang.org/ or even property-test libraries such as QuickCheck http://hackage.haskell.org/package/QuickCheck (for Haskell) and Hypothesis https://github.com/HypothesisWorks/hypothesis (for Python).

Feel free to DM me if you need more guidance.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/marcoonroad/subtype-refinement/issues/5?email_source=notifications&email_token=ALFT2ASXHIHPI7YUVYIPKHLQTHLMVA5CNFSM4JI67N52YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEDYK4MA#issuecomment-552644144, or unsubscribe https://github.com/notifications/unsubscribe-auth/ALFT2AWOS4ZPIA3SSLZIMGTQTHLMVANCNFSM4JI67N5Q .

marcoonroad commented 4 years ago

To use this library properly, you need a good knowledge of OCaml's modules and functors. A good resource covering such concepts is the OCaml's Real World book:

I also recommend playing around with an interactive REPL for prototyping, utop is the most known one. Once you have an environment set up on your machine, including OPAM, you can install this library, then type on Linux's terminal:

utop

And inside the REPL, typing:

#require "subtype-refinement";;

And after:

open Subtype_refinement;;

Now you can create type refinements based on arbitrary constraints. The test here covers better examples than the README itself (which I'll improve soon once I have some time).

Library details (you can skip if you wish)

The library basically creates a generative module with fresh private type of functor's parameter (the constraint/"typeclass" module). By generative, if we have two modules M1 and M2 which are the result of a functor application F(M0) (so M1 = F(M0) and M2 = F(M0)), both M1 and M2 will contain different types, that is, M1 != M2 (with applicative functors, both M1 and M2 will share the same type constraint, a behavior akin to Haskell's typeclasses, that is, M1 == M2). And by private, it means that only the module can construct/make such private types, and the user can later upcast these private types carrying invariants. This is sometimes called a "translucent" type.