内容简介:2020·04·15 · tutorials · type theoryAs we delve deeper into Type Theory, we tend to discover concepts that don’t have many details written out. Or, if there is writing about them, it is filled with technical jargon and advanced diagrams.
2020·04·15 · tutorials · type theory
As we delve deeper into Type Theory, we tend to discover concepts that don’t have many details written out. Or, if there is writing about them, it is filled with technical jargon and advanced diagrams. The Wikipedia page for Row Polymorphism is a great example of this. The first line states:
In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are polymorphic on record field types.
This description isn’t helpful, and the rest of the article fails to explain what it can be used for. Today, I’ll be doing my best to explain Row Polymorphism without the jargon.
Subtyping
To explain something new, it can be nice to put it in terms of what you know. Most developers have seen subtyping in the wild. It’s the core of OOP, the first thing you learned in your Java course: types can inherit each other. In Java, every class has a superclass that it inherits fields and methods from.
public class Human { Color hairColor; Color eyeColor; int height; int weight; } public class Employee extends Human { Job job; int salary; }
Human
here contains a number a fields relating to what a human might have. When we say Employee extends Human
, we say that the fields and methods in Human
are also in Employee
.
Here’s where the polymorphism
comes in: we can use Employee
anywhere a Human
is expected.
public feed(Human human) { human.weight += 16; } ... Employee employee = new Employee(); feed(employee); // works correctly!
This function expects a Human
, but we can give it an Employee
or any other type that inherits
Human
.
What if my rows are equal?
A row
in this context is a field in our structure. weight
and height
are rows in Human
. To
be polymorphic over rows means that we can provide many rows where only a few are expected. Let’s
look at an example.
public class Fish { int height; int weight; } ... Fish fish = new Fish(); feed(fish); // doesn't compile!
Oh no! Our fish won’t compile! Even though Fish
has the weight
field that feed
expects, this
won’t compile because Fish
doesn’t extend Human
. How do we fix this? We’ll, we’d need to make Fish
and Human
subtypes of the same class, something like Entity
.
public class Entity { /* ... */ } public class Fish extends Entity { /* ... */ } public class Human extends Entity { /* ... */ } // Now this works with Fish and Humans! public feed(Entity entity) { entity.weight += 16; }
Let’s sum up what’s happening here: to add a Fish
to our code, we had to:
-
Make a new class that
Fish
andHuman
both extend - Cut any fields from the subclasses and paste them in the new class
- Do the same for any methods that might be applicable
-
Refactor any methods using the existing classes to use
Entity
This is a lot of work to add a fish!
What if we could, instead, write our functions in a way that checked if our rows were equivalent?
Our feed function only cares about a subset of the fields we’re providing it: weight
. In Java
like languages, we’re required to use subtypes or make an interface that declares our field, but
what if we could write a generic function that only expected the subset of rows?
Polymorphism over Rows
Let’s look at an example in a language that does have Row Polymorphism: PureScript .
area thing = thing.width * thing.height
This defines a function called area
that will calculate the area for a thing. The type of this function reads:
area :: forall r. { width :: Int, height :: Int | p } -> Int
which says the first parameter is a record ( {}
) that contains two ints, width
of type Int
and height
of type Int
.
This record is also allowed to have other rows in it ( | p
). It returns the area as an Int
.
This function allows us to supply
any type that contains the width
and height
fields
. We are allowed to have whatever other
fields we want, because the function specifies a rho ( | p
) at the end of the record’s field list. This is Row Polymorphism!
Let’s make our fish again:
newtype Fish = Fish { width :: Int, height :: Int, length :: Int }
This time our fish has information about its dimensions. Can we pass in Fish
to area
? Yes!
We are free to use any
type that contains the expected fields! This changes things dramatically, and can greatly reduce refactoring. We can create
functions that apply to many different kinds of structures without needing to specify every structure it’s applicable to.
volume :: forall r. { width :: Int, height :: Int, length :: Int | r } -> Int volume thing = thing.width * thing.height * thing.length
volume
automatically accepts Fish
and any other types that contain the correct fields.
Building off of existing types
Row Polymorphism not only allows us to not only accept types with a variable amount of fields, but it also allows us to extend existing types with new fields. Here’s an example in a little language called Ordo :
(* we define a function that takes in a record and returns the record with a new field added to it *) let f r = { y = 0 | r } (* we can then call this function with a record, { x = 0 }, and the function returns a new record with the old fields and the new 'y' field *) f { x = 0 } = { x = 0, y = 0 }
I like Ordo’s syntax here because it’s very clear what is happening. Functions can arbitrarily extend records with aditional rows. This is another great property of Row Polymorphism!
Outro
Using Row Polymorphism as a
replacement for subtyping hasn’t been explored in many languages. I think this is because most programmers are used to
subtyping so many newer languages try to include it. Row Polymorphism can also lead to confusion where calling a function
works but semantically it doesn’t make sense, like finding the area
of a Fish
. A Fish
can have a surface area, but
that is a different formula that expects a length. In a language with subtyping, we might restrict area
to only work
on an Entity2D
and volume to only work on an Entity3D
, which would make sure our functions are only called with the types
we expect. I think both solutions bring something good to the table, and we should definitely explore both options more.
Here are some languages that have Row Polymorphism:
以上所述就是小编给大家介绍的《Row Polymorphism without the Jargon》,希望对大家有所帮助,如果大家有任何疑问请给我留言,小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持!
猜你喜欢:本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们。
Thirty-three Miniatures
Jiří Matoušek / American Mathematical Socity / 2010-6-18 / USD 24.60
This volume contains a collection of clever mathematical applications of linear algebra, mainly in combinatorics, geometry, and algorithms. Each chapter covers a single main result with motivation and......一起来看看 《Thirty-three Miniatures》 这本书的介绍吧!