Talk:Algebraic data type

From Wikipedia, the free encyclopedia

[edit] Tagged union

I believe this page and tagged union refer to more or less the same concept, but they could be merged usefully. Does anyone disagree with this?

Derrick Coetzee 16:37, 4 Apr 2004 (UTC)

I think that would be a bad idea. A tagged union is different from an algebraic data type, but they can be used to implement algebraic data types, though this article probably needs more generalization. Dysprosia 22:05, 4 Apr 2004 (UTC)

Yes, I agree that these deserve different articles. I plan to clean this one up. Brighterorange 04:40, 13 May 2005 (UTC)

[edit] Languages

Which languages support algebraic data types? Using What links here, I only see Haskell, ML, Nemerle, Hope, Pizza.

So Haskell uses : for list constructor operator and ML uses :: and they use the other for type annotations. I suppose it's ok to give both alternatives then. But do we need to give Nil and Cons without capital letters as that makes them look like functions? I know Lisp has nil and cons but then again Lisp doesn't have algebraic data types and constructors. If it's meant to be mathematical notation, I must say I'm not a fan of it either in programming-related articles.

My proposal would be to revert Nil and Cons to have capital letters. --TuukkaH 15:51, 15 February 2006 (UTC)

[edit] Misleading "Variations" section

I just removed the following discussion from the article. See below for why.

Languages with type systems based upon System-F, such as OCaml or SML, may not use constructors directly in substitution of normal functions within a given expression. Languages with more expressive type systems based upon something similar to System-Fω (i.e., systems that use kinds, where a kind serves as a "type of a type"), such as Haskell, may however use constructors directly in substitution of a normal function. The latter case also implies then that constructors in these more expressive languages may be partially applied (i.e., curried), whereas the same is not true for languages in the former case.

For example, the following is completely acceptable in Haskell (System-Fω-based):

map :: (a -> b) -> [a] -> [b]
map Leaf [0 .. 9]

But in OCaml (System-F-based), this approach yields:

List.map : ('a -> 'b) -> 'a list -> 'b list
List.map Leaf [0;1;2;3;4;5;6;7;8;9];;
   The constructor Leaf expects 1 argument(s),
   but is here applied to 0 argument(s)

And so, in OCaml (System-F-based), one must wrap the Leaf constructor in a lambda abstraction, since it cannot be substituted for a normal function, such as List.map expects. To make it acceptable then, it must be modified like so:

List.map (fun x -> Leaf x) [0;1;2;3;4;5;6;7;8;9]

The problem is that map Leaf [0,1,2,3,4] is legal SML, even if it is not legal OCaml (I wouldn't know about the latter). It follows that the reason for its being illegal in OCaml has nothing to do with predicativity or the restriction to prenex polymorphism, which is what the above seems to mean by being "System-F-based" -- that in itself, of course, is somewhere between misleading and false. Is there, in fact, a "reason" why OCaml cannot treat datatype constructors as values of function type, or is that just the way the language happened to be designed? -- Cjoev 17:22, 28 March 2006 (UTC)

Let me add here what the article had before this confusion was brought about:

Here, Empty, Leaf and Node are the constructors. They are used much like functions in that they can be (partially) applied to arguments of the appropriate type. For instance, Leaf has the functional type Int -> Tree meaning that giving an integer as an argument to Leaf produces a value of the type Tree. As Node takes two arguments of the type Tree itself, the datatype is recursive.

A constructor application cannot be reduced (evaluated) like a function application though since it is already in normal form (there is no function definition for it). Operations on algebraic data types can be defined by using pattern matching to retrieve the arguments, for example, consider a function to find the depth of a Tree:

At least it was clear even if it turns out it wasn't factually completely accurate. --TuukkaH 18:26, 28 March 2006 (UTC)

I tried to pick a simple example, but it appears the example I picked was too simple to illustrate the issue I was raising.

I suspect that what is happening in the case of SML is that the compiler is simply wrapping the constructor in a lambda abstraction in much the same way I did manually for the O'Caml example. But this still does not imply that constructors are treated the same in SML and O'Caml as are functions, and this is directly due to issues with the type system.

What do you mean, "treated the same"? In one sense, of course they are not, because constructors can appear in patterns but functions can't (duh). In every other sense, SML "treats" a constructor exactly as if it were a function of the appropriate type. The question of what function types can be inhabited by constructors is not the same as how such a value is "treated" once it exists. Cjoev 19:27, 31 March 2006 (UTC)

Here is a much more complex example that should not be possible in SML without many additional lambda abstractions, because of this issue:

data Triple a b c
    = MkTriple a b c
      deriving Show

zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]

foo = zipWith (\f x -> f x) (zipWith MkTriple [0..4] "abcd") ["foo","bar","baz","qux"]

... =>[MkTriple 0 'a' "foo",MkTriple 1 'b' "bar",MkTriple 2 'c' "baz",MkTriple 3 'd' "qux"]

bar = let f    =     MkTriple
          f'   = f   0
          f''  = f'  'a'
          f''' = f'' "foo"
      in f'''

... => MkTriple 0 'a' "foo"

baz = let f    =     MkTriple
          f'   = f   f
          f''  = f'  f
          f''' = f'' f
      in case f''' of
           (MkTriple g h i) -> let g' = g 0 'a' "foo"
                                   h' = h 1 'b' "bar"
                                   i' = i 2 'c' "baz"
                               in f g' h' i'

... => MkTriple (MkTriple 0 'a' "foo") (MkTriple 1 'b' "bar") (MkTriple 2 'c' "baz")

Haskell can do this because it treats constructors the same as functions -- (i.e., constructors can be curried, and they can have an arity > 1, whereas in OCaml and SML, arity is always only 0 or 1, and multiple parameters must be expressed via tuples, which means constructors here are not as general as true functions). Again, this is related to the type system.

Well, yes, this is related to the type system in the sense that it is a feature of the language. I disagree that it is the result of some deep difference (e.g. F versus Fω) between the type systems as the section I removed from the article contended. Cjoev 19:27, 31 March 2006 (UTC)

The selection of text I replaced was wrong because it implied that constructors can be partially applied, but this is not universally true -- it is not true in the case of OCaml (which was given as one example of using ADT's). Secondly, the bit about constructors not reducing to functions, because of having no function definitions, etc., is also incorrect -- it again depends upon the type system, which is what I tried to clarify.

OK, so constructors in OCaml must be fully applied (taking your word for it -- I don't use OCaml myself). But the part about constructors "reducing" to functions or not makes no sense either to affirm or deny. In SML, a constructor is a function (except when it appears in a pattern), and it's a value so it doesn't have to reduce. In OCaml something slightly different is the case. I don't see how either the original example or your new code clarifies this. Cjoev 19:27, 31 March 2006 (UTC)

So, in short, I do not think my addition was wrong, but the example I chose was too simple to fully illustrate the issue, and in the case of SML, it appeared misleading because of the fact that the compiler most likely handles these very simple cases automatically.70.36.30.117 17:36, 31 March 2006 (UTC)

The following is legal SML code approximating the third part of your new example:

datatype ('a,'b,'c) triple = Triple of 'a * 'b * 'c

fun mktriple a b c = Triple(a,b,c)

val baz = 
    let 
      val f    =     mktriple
      val f'   = f   f
      val f''  = f'  f
      val f''' = f'' f
    in case f''' of
         (Triple (g, h, i)) => let val g' = g 0 #"a" "foo"
                             val h' = h 1 #"b" "bar"
                             val i' = i 2 #"c" "baz"
                           in f g' h' i'
                           end
    end

Yes, it's true that constructors in SML cannot be curried, but all you need to do is write the curried function yourself and you can use it wherever you like. The only obstacle is the value restriction, which is legitimately different between ML and Haskell but has nothing to do with constructors (does it?).

If I understand you correctly, the issues you raise are: (1) partial application of constructors is only possible if they are curried, which does not occur in either variant of ML; and (2) the parenthetical "there is no function definition for it" from the earlier version is meaningless and certainly does not explain "why" a constructor application is considered a normal form. Both of these are true, but I contend they have nothing to do with the presence or absence of kinds, with F-versus-F-omega, or with restrictions to predicative prenex polymorphism. Cjoev 19:27, 31 March 2006 (UTC)

What I am saying is that, due to the fact that Haskell uses System-Fω, constructors are treated quite differently than in SML and OCaml. The way that they are treated in Haskell makes them appear much more like ordinary functions, without the restrictions that are placed upon them in SML and OCaml. The original text made some claims that were incorrect with regards to the relationship between constructors and functions, and I attempted to clarify it. But the example I chose was admittedly misleading.

In something like System-Fω, where one has kinds, a "type" is not actually a type unless it is of kind *. Example:

data Triple a b c = MkTriple a b c  -- not a type, but kind: * -> * -> * -> *
type F            =     Triple      -- ...             kind: * -> * -> * -> *
type F'           = F   Int         -- ...             kind: * -> * -> *
type F''          = F'  Char        -- ...             kind: * -> *
type F'''         = F'' String      -- now a type,     kind: *

f :: Int -> Char -> String -> F'''
f = MkTriple

When one adds kinds, they modify the term language itself to allow for abstraction over constructors with *any* kind, not just kind *, or "type". This allows one to use constructors in essentially the same way as functions (incl. currying). This is because, via kinds, there is now a notion of what it actually means for a constructor to be partially applied (i.e., its "type" is still of some kind * -> ... -> *, rather than *). Can one "fake" treating constructors as functions by wrapping them in lambda abstractions? Sort of, yes. But it's not the same thing at a fundamental level. Furthermore, without something like System-Fω, you don't get application at the type level, as I showed above. 70.36.30.117 23:22, 31 March 2006 (UTC)

Ah, now I see that part of our failure to communicate is the overloading of the word "constructor". There are type constructors, or what SML/NJ's error messages call tycons, such as Triple, and then there are value constructors such as MkTriple. The former has kind * -> * -> * -> *; the latter is a term-level construct that (in Haskell) has type a -> b -> c -> Triple a b c (which has kind *). This type is universally quantified, but all the variables have kind * and so I maintain that it is not significantly different from the SML type 'a -> 'b -> 'c -> ('a,'b,'c) triple, which is the type of mktriple in my translation of your earlier example.

Partial application of type constructors is possible in SML, but you have to write it in a stupid way that looks like you've η-expanded everything (and combined with ML's postfix application for tycons ends up being mighty confusing):

type ('b,'c) F' = (int,'b,'c) triple
type 'c F'' = (char,'c) F'
type F''' = string F''
val f : int -> char -> string -> F''' = mktriple

As you point out, the real difference between ML and Haskell is the ability to write terms that quantify over kinds other than * (I'm taking your word that Haskell can do this), which appears to be lacking in ML (but see my next paragraph). However, I claim that (1) you still have not produced an example that does this (but you don't have to because I readily concede such examples exist), and (2) more importantly, since it's an issue of type constructors rather than value constructors it has nothing to do with algebraic datatypes per se and does not belong in this article. Maybe it belongs in Polymorphism (computer science).

Finally, I've been putting off saying this, but if you count the module system, then SML is Fω-based. (Think about the fact that a functor argument can have a parameterized type in it.) This is made very explicit in a number of papers by Bob Harper and others (I can provide references if you like) and will likely become even more evident in future versions of the language if proposals for extensions to SML with higher-order and/or recursive and/or first-class modules are ever adopted. The distinction between SML and Haskell is not F versus Fω, it's artificially-restricted-Fω versus full Fω. The restrictions are there for historical reasons to do with type inference; Haskell has since done away with them, but ML has not. Cjoev 01:09, 1 April 2006 (UTC)