Hard disagree, C++ type system is quite strong and const-correctness is a thing.
Just because there is an escape (compare
http://www.cs.virginia.edu/~evans/cs655/readings/bwk-on-pascal.html, section 2.6), doesn't mean the type system is optional.
Can't you cast away const correctness?
I admit I don't know much about it.
I've looked into Haskell, with its "functional purity above all" dogma, and it seemed more like a plaything for mathematicians and participants of code golf competitions, rather than something to use in serious software projects.
Is OCaml more pragmatic?
Yes.
If you're familiar with promises (like Javascript's promises), Haskell's shtick is that basically every value is an implicit promise. That, plus Hindley Milner typing (Haskell extends it with typeclasses, which I don't really know anything about) and immutability.
The idea is that, with immutability, since you can't assign anything to any variables, code cannot rely on the side effects of any other code having been run. As long as the inputs to the function are computed, the order doesn't matter.
I agree that this is excessively pure for most purposes. It's good for things like writing compilers, but probably not much general usage.
Ocaml has normal execution semantics, just with HM typing. Code is executed in the order you'd expect. Ocaml also does have side effects, in that you can mutate arrays and things like that, although your typical Ocaml program doesn't do it very often. It's mostly done for efficiency in specific situations.
Usually I'll write a program in a very functional style, and then benchmark to find places where I might want to implement some side effecting code for speed.
So for example, I was working on a REST API for a project, and logically,
GET /someitems?count=5
is a very functional operation. I fetch the items from the database, and then I can map a function over that list to process them somehow and return it as JSON.
I noticed that my code was making a shitton of database requests (each object required a second database hit for some ancillary information), so I replaced the function that fetches that ancillary data with one that returns a closure that internally has a small cache. It spreads the ancillary database requests across all the main objects requested. (and it gets reset on each http request)
Most of my code consists of typical functional stuff like
List.map ~f:(fun post -> public_json_of_post post) (fetch_db_posts())
, except after benchmarking, I modified public_json_of_post to have a little internal cache.
And another question:
From your code examples, it looks like writing out type names in the source code is avoided in OCaml in favor of letting the compiler derive the types on its own.
Doesn't that get you into "What happens when the compiler is smarter than the programmer" kind of pitfalls?
Like, when the auto
keyword was introduced in C++11, it was hailed as a great advancement. You can write it in certain places where you'd normally write out a type name, and the compiler will determine the correct type on its own!
But in practice, I've become wary of this keyword, because I don't just want the type to be clear to the compiler, I also want it to be clear to reader of the code (including myself, when I return to that piece of code later).
So there should be some clarification about how the type inferencing works in Hindley Milner type systems.
To start with, in the standard library, the built-in functions, all are inherently typed.
So for example, when I type out in the ocaml repl:
Code:
# string_of_int;;
- : int -> string = <fun>
# int_of_string;;
- : string -> int = <fun>
Two functions, string_of_int takes an integer and returns it formatted as a string and int_of_string takes a string and tries to parse an integer from it.
The way HM typing works, is that they trace all the calls in your program, and all the variables and where they come from, back ultimately until you end up with the return or argument to one of the already typed functions. And it calculates types from there.
The type system isn't guessing in a humanistic way what the types of the variables should be, rather it's determining factually what they must be. If the type checker fails, that means at some point you're trying to pass a string to a function expecting an int. ie your program doesn't make sense.
There are nice uses for it, like when the written-out typename would be too long and unwieldy and you don't really care about it because it's just the type of some intermediate object (like an iterator) where it's clear from context what it is and how it's used, e.g.:
Code:
std::multimap<SomeType, std::unique_ptr<SomeOtherType>>::iterator it = table.begin();
auto it = table.begin(); // same thing
But I definitely wouldn't use
auto
in C++ everywhere where it's allowed.
Does it feel different to you in OCaml?
i.e. that even in larger, real-world projects, it remains sufficiently clear to humans what the types of your functions/variables are?
I generally do my Ocaml development using a repl. I have a text editor open, and then a window with the repl.
I can type out the name of a function (either built-in or one I wrote) and it tells me the types of the inputs and outputs.
I don't often specifically type my variables. Usually I just rely on a consistent naming convention for my variables. Although sometimes if I'm really dealing with a mess of complicated types, I might type some of my variables to get everything straight in my head.
And yeah, shortening up long, compiler generated types is one reason I might type something. But you can also do more interesting things with the type system.
So here's an implemention of a bitstring, based on the built-in byte arrays:
Code:
module Bitstring = struct
type t = bytes (* bytes are the built-in byte array type *)
let of_bytes bytes =
bytes
let length bs =
8 * Bytes.length bs
let get bs idx =
failwith "debug finish"
let set bs idx value =
failwith "debug finish"
end
This is a common Ocaml paradigm. You'll have a module called
Noun
and it has one single type called
t
and a bunch of functions in Noun that manipulate Noun.t's.
On this first try, it typed this module as:
Code:
module Bitstring :
sig
type t = bytes
val of_bytes : 'a -> 'a
val length : t -> int
val get : 'a -> 'b -> 'c
val set : 'a -> 'b -> 'c -> 'd
end
All the 'a 'b, etc are placeholder types because the typechecker can't assign a type for them yet. So for example, you can call of_bytes with an int and since it just returns its argument, it returns an int. But if you call it with a string next, it'll return a string.
Second try, I typed everything out:
Code:
module Bitstring = struct
type t = bytes (* bytes are the built-in byte array type *)
let of_bytes (bytes : bytes) : t =
bytes
let length (bs : t) =
8 * Bytes.length bs
let get (bs : t) (idx : int) : bool =
failwith "debug finish"
let set (bs : t) (idx : int) (value : bool) : unit =
failwith "debug finish"
end
And here's how that typing looks like now:
Code:
module Bitstring :
sig
type t = bytes
val of_bytes : bytes -> t
val length : t -> int
val get : t -> int -> bool
val set : t -> int -> bool -> unit
end
Now, you can do neat things with the signatures. Technically speaking, signatures aren't strictly necessary. You can distribute just the source code of the module as a .ml file and that's fine. However, you can package the signature up in a .mli file and you can modify what is or isn't public.
So I could make a bunch of internal functions for working with bitstrings and just not export them.
And more interestingly, the fact that Bitstring.t is just an alias for bytes can be hidden through the signature.
If my .mli file for this looks like:
Code:
module Bitstring :
sig
type t (* note the missing type alias *)
val of_bytes : bytes -> t
val length : t -> int
val get : t -> int -> bool
val set : t -> int -> bool -> unit
end
then all this signature says that a type known as
Bitstring.t
exists, and it tells us that we can create one by passing a bytes variable to
Bitstring.of_bytes
. It tells us nothing about how Bitstring.t's are implemented internally.
That being said, the compiler does know that it's just working on plain old byte arrays in the end. So the code it generates is as fast as doing native byte array work, just through a locked down, restricted interface.
The following code works or doesn't work depending on if the type alias is published:
Code:
let my_bytes = Bytes.of_string "abc"
let my_bitstring : Bitstring.t = my_bytes (* requires the type alias to be published *)
let my_bitstring : Bitstring.t = Bitstring.of_bytes my_bytes (* works regardless *)
let my_bitstring = Bitstring.of_bytes my_bytes (* without manual type annotation *)
I have a question for the type theorists, how would you type a function to specify it doesn't block?
How would you type a function which takes two functions as arguments but only one of them ever is called?
Is there a type system which allows you to model this?
In a turing complete language, I don't think that's possible.
If you're asking what typecheckers assign to functions that never return, in Ocaml, it's an indeterminate type. So
failwith
is typed
string -> 'a
because it never returns.