How to become 10x OCaml developer?

idris … dependent types in a real programming language. That. Is. Wacky. I remember Hans Boehm telling us about his PhD thesis project: the Russell language (and compiler). It was a dependently-typed language with a type-inference algorithm, but (heh) the algorithm might not terminate. There aren’t enough examples at the “Idris > Example” page to tell whether that is true of Idris’ type {checker,inference algorithm}, and the FAQ isn’t helpful, either.

Do you know of a better source of information on Idris’ type system?

Unfortunately, this is not only true of programmers. Generally speaking, when you claim something you must be able to justify your assertion, but most people can’t.

Hoare logic is useful when you have to deal with mutability and imperative programming. I would say that most of functional code uses immutable structures, and constructive logic is sufficient in this case.

By the way, Hoare logic and constructive logic are deeply related. For instance, the rule of composition:

{P} S { Q }  , {Q} T {R}
-----------------------------
      {P} S ; T {R}

is the hoare version of the double modus ponens rule (which is the type of reverse composition of function)

A -> B  , B -> C
---------------------
      A -> C

And to be honest, this rule (from Hoare logic) was already a consequence of kant’s transcendantal logic, see his table of categories where the category of cause and effect (mutability of state) is related to the logical form of hypothetical judgment (if A then B, A -> B) and the notion of state (first category of relation, substance and accident) is related to the logical relation between a subject and its predicate (Socrates is mortal, Socrates : mortal, val i : int …). I’m preaching for my church too :slight_smile: .

What’s the problem with that? You say that programmers should prove their code correctness, and that’s what you do with dependent types. See, for instance, software foundations books series.

2 Likes

Um. So there is lots of diversity of opinion on this. And for sure, I don’t want to dissuade people from using constructive logic to prove programs correct (meet their specification). But I’ll make the following observations:

(1) I wasn’t talking about using proof-systems to prove your programs correct, but rather, “desk-checking”. B/c any of the various methods of formally (mechanically) proving programs correct, are vastly more labor-consuming than writing an informal proof on paper (or comments). And as professional programmers who need to get paid, that’s unacceptable (except in certain rare situations, like safety-critical code).

(2) Eventually, if you write nontrivial code, you will end up writing imperative code. You will end up using mutable datastructures. I’m writing a compiler; almost all the code is side-effect-free. But (a) the code that sorts function-definitions into dependency-order uses an imperative topological sort, and (b) the type-checker for the next phase will rely on unification, which I’ll implement in the usual imperative manner (b/c geez, I’m trying to finish this thing).

Really, all I’m saying is: “learn how to prove your programs correct at the level of writing proofs in the comments that convince skilled practitioners”. If constructive logic makes that possible for you, that’s excellent. But the key goal is to be able to prove your programs correct, not the particular methodology you use.

5 Likes

There is good book about it: Type driven develpment with Idris.


I read most of it, but didn’t switch to the language,
because I don’t want to pay the reduced productivity (for some time) because of switching language.
Also, sometimes I feel the OCaml community is too small, so some things don’t take off and some parts of the ecosystem still lag behind compared to some other languages and communities.
With Idris, that would be worse. I guess their user community is way smaller.

2 Likes

I found a copy of the book and quickly paged thru -every- page. Nowhere did I find a description of the type system in the -standard- form that as a PL guy, I would expect: a collection of typing judgments in the manner of a proof system. The sort of thing that has been standard in PL for decades. This is the same problem I have with Rust (and, heck, with Golang).

I see no neutral description of what sort of type inference Idris has. The book is, to be frank, a -tutorial-. Which is, sure, great for when I want to -learn- the language. But is USELESS for -assessing- the language.

Maybe an example of why I’m so insistent this is in order. So: an example from Golang. Golang claims that in binary arithmetic expressions (e.g. M + N) the type of either side, when a constant, can be inferred from the type of the other side. But this isn’t enough to type expressions like (1 << n) + m (where n, m are both variables. The left side of the addition is not a constant, but one cannot infer the type of 1 from context. Turns out, they have a further rule – that if one side is a constant OR a “head constant” (like the LHS here), then the other side’s type can be used as a hint. There’s a little more, but this is the gist. And none of this is described in the specification.

There are other examples of lacunae in the spec. And this may be fine for … journeyman programmers, but it is not fine for a PL guy who wants to KNOW what his program does, and wants to be able to KNOW when he’s written well-typed code without having to run it thru a compiler to find out.

I only mention such systems because I don’t see what is “wacky” in using them. It’s fine if you just put a sketch of proof in the comments of your code.

What I’m saying is that if Hoare logic and constructive logic can be seen, from a programmer point of view, as deductive systems to reason about your code, they are not exclusive, not used in the same context and I don’t see why one is more effective than the other.

  • Hoare logic when you write imperative code with mutable state ;
  • Constructive logic when you write pure functional code.

For instance, when you want to prove (in mathematics) that a property P stands for all integer, you use induction principle. You prove that P is true for 0 and that it passes to successor if P n then P (n + 1), then you conclude that P n for all n. This proof schemata is precisely what you do when you use fold_left on a list, and you only use principles from constructive logic (with induction principle).

There is a second version of this schemata where instead of having P n -> P (n + 1), the second premises is that you suppose that if P stands for all m ≤ n then P (n + 1). In this case, your are using fold_right on a list.

As we can see, this second version uses more premises to conclude (P 0, P 1, … P (n - 1) and P n), so this code don’t use constant space on the stack… :wink:

2 Likes

You should ask the creator of the language.
Maybe there is somewhere in one of his papers.

1 Like

Good idea. Nothing in his publications list (or under the “Idris” topic) on his homepage seemed like it met the requirement, so I emailed him. Thank you for suggesting it. It’s been so long since I was in academia, I no longer have the reflex to engage in scholarly communication.

1 Like