The rationale is in the verb to be that I emphasize in my sentence (“it is a function wich returns an int if you pass it a cat”).
Suppose you have a philosopher’s stone that can turn metal into gold, therefore it can more specifically transform mercury into gold: that is exactly what this principle claims (metal -> gold <: mercury -> gold).
If I have a metal I can transform it into gold (my_stone : metal -> gold)
but mercury is a metal (mercury <: gold)
therefore I can transform mercury into gold (my_stone : mercury -> gold)
So the concept mercury -> gold has a larger extension than the concept metal -> gold, i.emetal -> gold <: mercury -> gold.
This is probably because I don’t get some basic concepts, but the exact opposite seems true to me. Could you please elaborate more on the words “has a larger extension”. I tried reading on what “extension” means and it still seems to me that metal → gold should be the supertype of mercury → gold
The first proposition say that the concept of animal has a larger extension than the concept of men, the second one that Aristotle belong to the extension of the concept of men, hence the conclusion: he also belong to the extension of the concept of animal.
With the syntax of OCaml and of type theory, we’d write the syllogism this way:
Aristotle : men men <: animal
----------------------------------
Aristotle : animal
A typing judgment v : t says that a value v belongs to the extension of the concept denoted by the type t, and a subtyping judgment t <: s that a concept is included in another.
A system that can transform a metal to gold can also transform mercury to gold, but also iron to gold, lead to gold… : it works for any metal. But, one that can transform mercury to gold can not necessarily transform iron to gold or lead to gold. Hence there is more things that can transform mercury to gold, and so this concept has a larger extension.
By the way, there was an error in my previous message, the second premise should be written:
OK, let’s do it another way. Let’s say we have a type “animal” which has a property “mouth”
{species = "barracuda", mouth = []}
Then we also have type mammal which also has feet
{species = "lemur", mouth = [], feet = 4}
Seems like the mammal is a subtype of animal because functions that operate on animals can operate on mammals. So mammal option is a subtype of animal option, hence option is covariant as it preserves the relation. List constructor is also covariant (from what I read) so a list of animals should also accept a mammal.
And that’s where I lose it. I don’t get contravariance… Could you give some example of contravariance constraint where it would be more obvious what I can and can’t do with animals and mammals?
If I have to speculate, it will be useful in cases where I want something that works on animals but rejects mammals. Am I right here? Can you show an example with implementation, as I am still learning and am not sure how to do that. I suspect your examples in earlier comments do just that, but they seem quite general (and probably omit details) which confuses me.
Suppose you want to be able to transform lists of animals to some sort of string representing the whole zoo. Maybe there are multiple possible ways of representing a given animal as a string, so you would want a higher-order function with a type like string_of_zoo : (animal -> string) -> animal list -> string.
Now suppose you have a function string_of_mammal : mammal -> string; maybe it uses the feet field as part of its result. Could you pass this as the first argument to string_of_zoo? You cannot: otherwise, you might have a situation where there is a non-mammal in the list, and attempting to apply string_of_mammal would be nonsensical.
While a mammal can be used wherever an animal is called for, a function expecting a mammal cannot be used wherever a function expecting an animal is called for. It is rather the opposite: if you need a function that expects a mammal, a function that expects an animal will do. (E.g., suppose we had some more specialized function with type (mammal -> string) -> mammal list -> string. It would be safe to pass a function with type animal -> string as the first argument, because every element in the list has all the properties of an animal, and so can be passed to this function.)
I confess that I still find this pretty unintuitive (hence my need to edit the comment just now :), but hopefully thinking through the example will help.
type animal = <species : string; mouth : bool>
type mammal = <species : string; mouth : bool; feet : int>
type meat = Meat of string
type -'a hunter = 'a -> meat
let misterT : animal = object
method species = "barracuda"
method mouth = true
end
let king_julian : mammal = object
method species = "lemur"
method mouth = true
method feet = 4
end
let hunter1 : animal hunter = fun x ->
Printf.printf
"A %s is an animal %s, hence I hunt it!\n"
x#species
(if x#mouth then "with a mouth" else "without mouth");
Meat x#species
let hunter2 : mammal hunter = fun x ->
Printf.printf
"A %s is a mammal: it has %d feet and %s, hence I hunt it!\n"
x#species
x#feet
(if x#mouth then "a mouth" else "no mouth");
Meat x#species
OK, this blew my mind. By playing with… it’s so powerful! Thanks!
I needed this piece of code in order to (hopefully) understand it. Still can’t grok the terms (they are really counterintuitive to me), but I seem to be able to understand the code, how it works and why it works.
The question that I have now - why did you use objects? Is it just a myth that people rarely use them? This seems so powerful and useful that I itch on using it right away in the software I’m writing.
I’ll try to replicate this with functors and records and see how it goes.
Because there is no subtyping relation between records in OCaml, you must use object (or modules) if you want subtyping between record like structures.
You can also do this with modules and functors:
module type Animal = sig val species : string val mouth : bool end
module type Mammal = sig include Animal val feet : int end
I let you write the corresponding functions.
I forgot to write coercion examples with my previous code:
hunter1 misterT;;
A barracuda is an animal with a mouth, hence I hunt it!
- : meat = Meat "barracuda"
(* hunter1 is also a mammal hunter *)
(hunter1 :> mammal hunter) king_julian;;
A lemur is an animal with a mouth, hence I hunt it!
- : meat = Meat "lemur"
hunter2 king_julian;;
A lemur is a mammal: it has 4 feet and a mouth, hence I hunt it!
- : meat = Meat "lemur"
(* but hunter2 can't fish barracuda *)
hunter2 misterT;;
Error: This expression has type animal but an expression was expected of type
mammal
The first object type has no method fee
(hunter2 :> animal hunter) misterT;;
Error: Type mammal hunter = mammal -> meat is not a subtype of
animal hunter = animal -> meat
Type animal = < mouth : bool; species : string > is not a subtype of
mammal = < feet : int; mouth : bool; species : string >
Is there a significant performance difference between objects and modules? And in general (for this use case) what would be the tradeoffs between the two ways?
Edit: I read on the topic and seems like modules have more compile time checks and less runtime overhead, so I probably want modules.
For this kind of record like structures, I think that objects will be easier to use with the rest of the core language.
What don’t you understand with the terminology? Informally, you can view a type like a set whose elements are the values that inhabit the type, and the subtyping relation is the inclusion relation between these sets. Hence, if v : t (i.e.v is an “element” of t) and t <: s (i.e.t is “included” in s) then v : s (i.e.v is an “element” of s).
Is there a significant performance difference between objects and modules?
You’d need to benchmark to know whether the difference is “significant” in your case.
Modules are essentially just ordinary records and the items are at statically known offsets – this means that projection from a module is fast but subtyping between them can require allocating a new record with a different ordering.
Objects instead have a map mapping the hashes of method names to offsets into the method table. This makes method calls slower but allows subtyping to be a no-op. There is also a cache at each method call site that remembers the last map that was used at that site, and what the result of lookup was, so if you consistently use objects from the same class it should go quicker.
Actually, since I wrote that, I played more with code and now I know what confused me. Previously I thought that you can actively change the variance, but this doesn’t seem to work. OCaml seems to be able to figure out the variance, so the + and - signs in the type definitions seem to be purely for human consumption (though still verified and enforced by the compiler) and not something you use to actually control types. So the variance seems to be indeed, just a property of the types and not something you can tweak actively, and this now makes sense.
Another thing that confused me is that, as it turns out, I have to actively coerce types in order to feed subtypes to operators, while I previously thought that OCaml should figure that out by the type definitions and the + / - signs in them. The opposite seems to be true.
