I have been using OCaml for a while, and I have used it to write some utilities, libraries, and web apps for personal use. Previously, I used Python and Common Lisp. I use OCaml without really understanding anything about types; an understanding of the type inference stuff was not important for completing most of my programs. I have been treating OCaml as a “Lisp with pattern matching and strict typing”. I realize that my lack of understanding of types could be a limiting factor in bringing my OCaml programming to the next level.
I see that some OCaml libraries are designed with a “type safe” API and I wonder how that is done. I don’t have the basic foundation to understand things like GADTs, effects, etc. that are potentially useful for making libraries that encourage type safety. What books and resources can I use to fill up this knowledge gap?
Not sure what you saw here. Maybe telling us more would allow for more precise answers.
In any case for GADTs you can have a look at this chapter of real world OCaml. It starts with an example where using regular variants allows the occurence of dynamic errors and then goes on to show how you can avoid them by using GADTs.
I was looking at GitHub - anuragsoni/routes: typed bidirectional router for OCaml/ReasonML web applications, a type safe URL router whose API I tried to replicate to understand how it achieved type safety.
Maybe this blog post by @drup could help.
I thought I should add a little counterpoint: you don’t need to understand GADTs (nor use them) to effectively use OCaml typing to improve your programs. I don’t have pointers, b/c it’s been so many decades since I learned how these FP language type systems worked, but if I were teaching someone, I would find resources on:
- Hindley-Milner type inference
- algebraic datatypes and their use in programming
- modules/functors, generative types, and how they work in ML-family languages
- value-oriented programming (programming with values and induction over values, without mutation)
And sure, after that, GADTs. These are all well-trodden subjects, most going back well over 20 years, so there should be good treatments in textbooks about programming languages and type systems. Specifically, I’m suggesting looking in textbooks, and not in the sort of “how-to” book that typically we find for a new programming language. Though, it’s still worth reading Real World OCaml.
It’s possible that The Little MLer might be a good reference.
I’m sorry I can’t actually provide more references.
ETA: you’re right to want to learn this. Back in the early 90s, when programming in caml-light, I used to say “types are obstructions in the maze of programming: too few and there are too many dead-ends; too many and there’s no way thru; just enough, and there’s only one way thru and no dead-ends”. Proper use of types can make writing correct programs much, much, much more labor-efficient. So it’s a great thing to learn how to do this.
Oh, another pointer: Gerard Huet wrote a paper The Constructive Engine wherein he teaches how to work with lambda-calculus terms. What it really is, is a course in how to work a complicated inductively-defined datatype, with a complicated induction principle that is based on an equivalence relation. Really understanding that paper and its implications for implementation, was a big step forward for me, in my ability to program in ML.
I read that book a few years ago. I do not remember learning anything significant from it. For context, at that time I had some experience in basic OCaml (played around with it, and read Part I of the OCaml manual), read Learn Standard ML in Y Minutes, and read some parts of Programming in Standard ML by Robert Harper. Prior to all this, I had experience in functional programming using Scheme (after reading SICP, The Little Schemer, and The Seasoned Schemer), and playing with Racket.
I am thinking of reading Types and Programming Languages by Benjamin C. Pierce, but I don’t know whether or not that will get me closer to understanding types in OCaml.
By the way, I am an amateur. My formal education in computing consists of one university course in introductory computer science, and one course in Java programming.
it will certainly help you to understand types more which can only be helpful.
Maybe you can also find value in @yallop’s advanced functional programming course material.