Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Welcome To Ask or Share your Answers For Others

Categories

0 votes
265 views
in Technique[技术] by (71.8m points)

.net - What are row types? Are they algebraic data types?

I often hear that F# lacks support for OCaml row types, that makes the language more powerful than F#.

What are they? Are they algebraic data types, such as sum types (discriminated unions) or product types (tuples, records)? And is it possible to write row types in other dialects, such as F#?

See Question&Answers more detail:os

与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
Welcome To Ask or Share your Answers For Others

1 Reply

0 votes
by (71.8m points)

First of all, we need to fix the terminology. There is no such thing as "row type"?, at least in type theory and especially in the type system of OCaml. There exists "row polymorphism" and we will discuss it below0.

Row polymorphism is a form of polymorphism. OCaml provides two kinds of polymorphism - parametric and row, and lacks the other two - ad hoc and inclusion (aka subtyping)1.

First of all, what is polymoprhism? In the context of type systems, polymorphism allows a single term to have several types. The problem here is that the word type itself is heavily overloaded in the computer science and programming language community. So to minimize the confusion, let's just reintroduce it here, to be on the same page2. A type of a term usually denotes some approximation of the term semantics. Where semantics could be as simple as a set of values equipped with a set of operations or something more complex, like effects, annotations, and arbitrary theories. In general, semantics denotes a set of all possible behaviors of a term. A type system? denotes a set of rules, that allows some language constructs and disallows others based on their types. I.e., it verifies that compositions of terms behave correctly. For example, if there is a function application construct in a language the type system will allow an application only to those arguments that have types that match with the types of parameters. And that's where polymorphism comes into play. In monomorphic type systems, this match could be only one to one, i.e., literal. Polymorphic type systems provide mechanisms to specify some regular expression that will match with a family of types. So, different kinds of polymorphism are simply different kinds of regular expressions that you may use to denote the family of types.

Now let's look at different kinds of polymorphism from this perspective. For example, parametric polymorphism is like a dot in regular expressions. E.g., 'a list is . list - that means we match literally with list and a parameter of the list type could be any type. The row polymorphism is a star operator, e.g., <quacks : unit; ..> is the same as <quacks : unit; .*>. And it means that it matches with any type that quacks and does whatever else3. Speaking of nominal subtyping, in this case, we have nominal classes (aka character classes in regexp), and we specify a family of types with the name of their base class. E.g., duck is like [:duck:]* and any value that is properly registered as a member of class matches with this type (via class inheritance and the new operator)4. Finally, ad-hoc polymorphism is in fact also nominal and maps to character classes in regular expressions. The main difference here is that the notion of type in ad-hoc polymorphism is applied not to a value, but rather to the name. So a name, like a function name or the + operator, may have multiple definitions (implementations) that should be statically registered using some language mechanism (e.g., overloading an operator, implementing a method, etc). So, ad-hoc polymorphism is just a special case of nominal subtyping.

Now, when we are clear, we can discuss what row polymorphism gives us. Row polymorphism is a feature of structural type systems (also known as duck typing in dynamically typed languages) as contrasted to nominal type systems, which provide subtyping polymorphism. In general, as we discussed above, it allows us to specify, a type as "anything that quacks" as opposed to "anything that implements the IDuck interface". So yes, you can, of course, do the same with the nominal typing by defining the duck interface and explicitly registering all implementations as instances of this interface using some inherit or implements mechanisms. But the main problem here is that your hierarchy is sealed, i.e., you need to change your code to register an implementation in a newly created interface. That breaks the open/closed principle and hampers code reuse. Another problem with the nominal subtyping is that unless your hierarchy forms a lattice (i.e., for any two classes there is always a least upper bound) you can't implement type inference on it5.

Further Reading


0) As was pointed in comments by @nekketsuuu, I was using the terminology a little bit voluntaristic, as my intention was to give an easy to understand and high-level idea, without going deep into details. I've revised the post since then, to make it a little bit more strict.

1) Yet OCaml provides classes with inheritance and a notion of subtype, it still not a subtyping polymorphism according to the common definition, as it's not nominal. It should come more clear from the rest of the answer.

2) I'm just fixing the terminology, I'm not claiming that my definition is right. Many people think that type denotes a representation of a value, and historically this is correct.

3) Perhaps a better regexp would be <.*; quacks : unit; .*> but I think you got the idea.

4) Thus OCaml doesn't have subtyping polymorphism, although it has a notion of subtype. When you specify a type it will not match with the subtype, it will only match literally, and you need to use an explicit upcasting operator to make a value of type T to be applicable in a context where super(T) is expected. So although there is subtyping in OCaml it is not about polymorphism.

5) And although the lattice requirement doesn't look impossible, it is hard in real life to impose this restriction on hierarchies, or if it is imposed the precision of the type inference will be always bound with the precision of the type hierarchy. So in practice, it doesn't work, cf. Scala

? (skip this note on a first read) Though in OCaml there exist row variables that are used to embed row polymorphism into OCaml type inference that has only parametric polymorphism.

?) Often the word typing is used interchangeably with the type system to refer to a particular set of rules in the overall type system. For example, sometimes we say "OCaml has row typing" to denote the fact, that the OCaml type system provides rules for "row polymorphism".


与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
OGeek|极客中国-欢迎来到极客的世界,一个免费开放的程序员编程交流平台!开放,进步,分享!让技术改变生活,让极客改变未来! Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Click Here to Ask a Question

...