Conjunction types

Hi there,

Sorry to pester y'all, but I was hoping I might get some citation-type help. I realized for my little pet language that I'm working on that need to do some homework on conjunction types, but I can't find any publicly-available articles on the topic. Does anyone know off of the top of their heads any friendly introductions to these types that doesn't require IEEE or ACM membership to read?

Thanks in advance,

JimDesu

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

what is a conjunction type?

Perhaps you mean intersection types or maybe even just ordinary product types? Some more info would be nice.

Found it in the Getting Started post....

From the paper Polymorphic Type Inference by Michael Schwartzbach, on page 21:

"One example is the conjunctive type written "|- e: s /\ t" [sorry, I don't know how to html-ify that] which means that e simultaneously has types s and t".

This is exactly what I was thinking about for allowing record field labels not to have to be unique: by letting them be selector functions having more than one type. Is this the same thing as an intersection type and I just didn't get it? I have to confess that I can only read the math R E A L L Y S L O W L Y.

Polymorphic variants

Hmmm, ok, I wasn't familiar with term, but it seems that a conjunctive type is like a sum type except that there are no constructors to distinguish the cases. A.k.a polymorphic variants.

Here's one paper I found: http://caml.inria.fr/pub/papers/garrigue-deep-variants-2004.pdf

Maybe not what you're looking for but it shows there is active research going on in this area so I think the chances of finding any really introductory articles aren't good.

Oops

No actually, conjunctive type != polymorphic variant though they are related.
After reading some of the paper I linked above, it's clear that a conjunctive type "e: s & t" means that e could be an s or a t but we're not making a commitment as to which one yet. So it's a way of approximating types (ie. "we don't know the type exactly but we do know that it will be one of these ..."). In any concrete program, type inferencing will eventually narrow the type down to a specific case.

Intersection types, seconded

After reading some of the paper I linked above, it's clear that a conjunctive type "e: s & t" means that e could be an s or a t but we're not making a commitment as to which one yet.
This indeed sounds like intersection types. They were introduced more than 20 years ago (IIRC, I've seen a reference to a paper dated by 1978), but started gaining new popularity recently. You may search LtU (I've posted a few items about intersection types), or Google, or just read an introduction to Programming with Intersection Types and Bounded Polymorphism (as it seems you are interested in polymorphism anyway).

Not sure, why leemarks changed his guess from intersection types to polymorphic variants? Am I missing something obvious?

John Reynolds

I agree with Andris that this looks very much like intersection types. A lot of important research that you'll want to look at is at the FLINT project page. Also ask Google about refinement types which are related and fairly cool themselves.

Incidentally, I believe Philip Wadler said once that John Reynolds tends to be about 10 years ahead of time in research. This is yet another example; one of the earlier examples of intersection types was in a language called Forsythe, that you also should look at.

understood, mostly

I was under the impression that an intersection type contained only those features of both its component types that they had in common, instead of literally being both types at once -- is this wrong?

Treating types as sets of va

Treating types as sets of values (naively) the intersection type is the intersection of the sets. I.e. it's values are the values of that are both types. So, yes, an element of a /\ b is an element of a and an element of b.

Sets of values, not of features

I suspect the confusion comes from thinking about "sets of features". See the previous post by Derek - "intersection" really means intersection of extents (i.e., all values) of the types, not of their features. In fact, if you define the notion of "a feature of the type" as "a proposition about every value of the type", the set of features of type A ∩ B will include all the features of both type A and type B: features(A ∩ B) ⊇ features(A) ∪ features(B)
If one wishes to remember Curry-Howard (and why not?), what I defined as "features" is actually a set of supertypes, i.e., features(A) ::= {T ∈ Types | T ⊃ A}, from which getting to my first statement is trivial.

[on edit: fixed a bug, so the statement was not trivial afterall]

Citeseer

Here's good place to look for all kinds of papers, citations etc. citeseer.ist.psu.edu. A quick search for intersection types (the most common name for conjuctive types I've come across) yields plenty of hits.

The only language I know that used them was Reynold's Forsythe and I don't know if that was ever implemented. I think he used it to replace product types or make the product commutative which ever way you look at it.

His book Theories of Programming Languages explores them in one of the chapters. He mentions the type-checking and inference problems that're related as well.

My confusion

I was well aware of the definitions given above for intersection types (the intersection type is the set of values common to both types). However it wasn't obvious (to me) that this definition could be applied to the conjunctive types in the paper I referenced earlier.

But I'll now also agree that conjunctive types are intersection types.
What threw me off is an example in the paper involving the type "int & string". int and string are disjoint so interpreting that as an intersection didn't seem right. After all, what point is there in a function that takes an uninhabited type?
However, on a more careful re-reading, it seems this can indeed be useful, consider this example derived from the one in the paper (I'm using Haskell syntax here):

-- define a variant type T and two functions f and g:

data T a = Orange a | Apple

f :: T Int -> String
g :: T String -> String

-- and now define h
h x = (f x, g x)

in Haskell h won't typecheck, but in the paper it's given a type of

h :: T (Int & String) -> String

although the type variable to T is uninhabited, h is still well-defined when applied to just Apple's. Moreover the fact that an "Int & String" value could never be constructed is precisely what's needed to get the type system to guarantee that only Apple's will ever be fed in.

Ok; I see the difference

I was thinking, if something like the following were legal:

name :: T -> String
name :: V -> Name

first :: Name -> String
middle :: Name -> Char
last :: Name -> String

then you'd have
name :: T & V
and
first . name :: V -> String
and
putStr . name :: T -> IO ()

Perhaps union types?

(As in the dual of intersection types)
So it would make more sense to say T | V rather than T & V. But regardless of the syntax, as you've illustrated, inferencing narrows the type based on usage constraints.

I don't see why this couldn't work but I do see one problem:
If I were to add a third name function, eg:

name :: X -> Name

then the typing of first . name would change to (X | V) -> String
I believe the fact that merely adding a new function can cause the types of previously existing functions to change shows the system lacks principal types.

Principal types

Ok please don't shoot me for such an ultra-newbie question, but, so long as it doesn't invalidate other code-paths, why would not having principal types be a bad thing? At the risk of sounding like a troll, why do you care what the principal type is so long as the type you express works?

Not a newbie-question IMHO

All implementations of type inferencing I've seen rely on either prinicpal types (or the related idea of principal typings). I guess there are reasons why that's the case but I'm not sufficiently clued up to really know why.
But I agree, if you can make it work, that would be great.

Why "principal"

why do you care what the principal type is so long as the type you express works?
Example1 in The essence of principal typings demonstrates the need. You might also want to read the whole "The HM system does not have principal typings for all terms" thread, as it contains references to both this paper and What are principal typings and what are they good for?, which by coincidence uses intersection types.

Both papers are more focused on "why principal typings", but you can find also arguments for "why principal typings".


My simplified understanding is that types (or typings) represent the information about parts of the program, produced by the type inference algorithm (they are kind of abstractions of these parts, or propositions, if you please). The trick is, the inferencer not only produces these propositions, but also uses them itself to derive new propostions about other parts of the program. The quality of being principal means that the inferencer does not add any arbitrary constraints to these propositions, and does not "forget" anything, leaving the propositions as good as possible in the given type system (or logic?). In other words, the principal typing of a program is the most perfect knowledge of this program expressable in the given type system. So, returning to your question: why care, if one can make a PL implementation work without principal types? I suspect the only way to make it work is to bootleg some part of the information, instead of honestly passing it around in types/typings (in fact, since a typing includes besides a type the other parts of, um, typing judgement, then typings are more honest in this respect :-) ).

I still suggest reading the papers I mentioned, as my interpretation might be quite wrong.

My simplificated understanding

Simplifying Andris Birkmanis's remarks further: A principal type is the most general type that properly captures the type of the expression (in the given type system). Thus, in a nutshell, not having principal types means you need to make an arbitrary decision/cutoff. I should not have to spell out why this is less than desirable.

Meta note: Attempting to post this reply, I get "terminated request because of suspicious input data". After a bit of experimenting, apparently from writing expression followed by parentheses (which I got around with <span>). A more informative error message or less restrictive filter would probably be helpful.

Haskell already has union types

jimdesu wrote:
I was thinking, if something like the following were legal:
It is legal already:
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module J where

import Prelude hiding (last)

data Name = Name{first :: String, middle :: Char, last :: String}

data T = T
data V = V

class Naming f t | t -> f where
    name :: f -> t

instance Naming T String where
    name _ = "Name of T"

instance Naming V Name where
    name _ = Name{first="V1", middle = 'X', last = "VLast"}

f1 = first . name
f2 = putStr . name

We can check that the inferred type for f1 and f2

*J> :t f1
f1 :: V -> String
*J> :t f2
f2 :: T -> IO ()
are the ones that we expected.

Cool

This also gets around the principal type issue I mentioned above by requiring that each instance of the name function target a unique type. So we allow overlaps on the domain but require disjointness on the codomain.

followup

My Haskell isn't that strong: what is the purpose of the "| t -> f" in the Naming class?

Functional Dependencies

See the Haskell Wiki: FunDeps along with
Fun with Functional Dependencies

Polymorphic variants

Exactly like with OCaml's polymorphic variants:

# let f = function `Orange n -> (string_of_int n)^" oranges" | `Apple -> "some apples" ;;
val f : [< `Apple | `Orange of int ] -> string = <fun>
# let g = function `Orange s -> s^" oranges" | `Apple -> "apples" ;;
val g : [< `Apple | `Orange of string ] -> string = <fun>
# let h x = f x, g x ;;
val h : [> `Apple | `Orange of string & int ] -> string * string = <fun>

Oops...

Sorry. Done.

IntegralString

int and string are disjoint so interpreting that as an intersection didn't seem right.

I suspect that if we are only interested in how they walk and quack, they don't need to be disjoint. In fact, even structural typing is not necessary: e.g., if Integer and String were interfaces in Java (instead of final classes), then it would be possible to have a class implementing them both.