Quote:Original post by Daerax
Seeing as the thread is dead. Would you happen to know the history of the term? Why are they called algebraic types?

There is an algebra of types, with sum as choice (Either), product as pairing (,) and exponential as the function type (->). You'll be familiar with this from CCCs in category theory. Algebraic data types are sums-of-products.

This is useful because it allows you to do things like calculate when two types are isomorphic and calculate the derivative (as in calculus) of a type to obtain a Zipper.

Regular inductive types subsume sum so it is not built into ML, but product is. Coinductive types like Charity's subsume product, so tuples don't have to be built in either. In categorical semantics, an inductive data type is an initial algebra for an endofunctor and a coinductive type is a final coalgebra for an endofunctor.

Quote:Original post by Rebooted

Quote:Original post by Daerax
Seeing as the thread is dead. Would you happen to know the history of the term? Why are they called algebraic types?

There is an algebra of types, with sum as choice (Either), product as pairing (,) and exponential as the function type (->). You'll be familiar with this from CCCs in category theory. Algebraic data types are sums-of-products.

Yeah essentially discriminated unions. Which is simple enough but I do not still see algebra as fitting.

Quote:This is useful because it allows you to do things like calculate when two types are isomorphic and calculate the derivative (as in calculus) of a type to obtain a Zipper.

That is some crazy stuff, made me go dizzy. So many strange concepts and connections, overwhelming. Will take me some time before I can comprehend that. I am actually in the process of self learning type theory.

Quote:Regular inductive types subsume sum so it is not built into ML, but product is. Coinductive types like Charity's subsume product, so tuples don't have to be built in either. In categorical semantics, an inductive data type is an initial algebra for an endofunctor and a coinductive type is a final coalgebra for an endofunctor.

Wait. Are inductive data types recursive types? How do inductive types subsume sum? Via simply adding recursion? Then they need not be algebraic. Checking wiki it looks like an "algebraic datatype" is a type formed in terms of some F-Algebra which is in turn defined in terms of an endofunctor which takes a generic X to 1 + X in our category (here X may or may not be formed by a product), hence the initiality in the Category of F-Algebras. Since F-Algebras are generalizations of Universal Algebras which generalize quaternions I can see an analogy from algebraic types to multiplication with integers so the term algebra makes sense here.

They call types formed in that manner algebraic Datatypes. Where do inductive types fit in this? What additional structure do inductive types add to algebraic datatypes

Quote:Original post by Daerax
Wait. Are inductive data types recursive types?

Yes. I think 'inductive type' is a synonym for 'algebraic type', although Charity's inductive types aren't quite the same as ML's algebraic types. Algebraic types are inductive and their dual in Charity are coinductive.

Quote:How do inductive types subsume sum?

In Haskell syntax:

data Sum a b where  Left  :: a -> Sum a b  Right :: b -> Sum a b

If you have coinductive/coalgebraic types too, then product is:

codata Product a b where  First  :: Product a b -> a  Second :: Product a b -> b

Quote:I do not still see algebra as fitting.

How come?

This is the relationship between type theory and category theory as I understand it:

• Types are objects. Functions are morphisms. Type constructors are functors. Parametricity is connected to naturality.


• 1 is the unit type, 0 is the bottom type, * is pairing, + is choice, exponential is the function type.


• An algebraic type is an initial algebra for an endofunctor. It has some construction operations and a fold to destruct it by structural recursion.


• A coalgebraic type is a final coalgebra for an endofunctor. It has some destruction operations and an unfold to construct it by guarded corecursion.

Update: Apparently 'inductive types', as found in Charity are less expressive than full algebraic types in Haskell. An inductive type is a fixed point of a functor, and nested types cannot be expressed in this way. So algebraic types are more expressive than inductive types and coalgebraic types are more expressive than coinductive types.

[Edited by - Rebooted on January 3, 2008 7:01:49 PM]

Quote:Original post by Rebooted

This is the relationship between type theory and category theory as I understand it:

• Types are objects. Functions are morphisms. Type constructors are functors. Parametricity is connected to naturality.


• 1 is the unit type, 0 is the bottom type, * is pairing, + is choice, exponential is the function type.

Yeah but you're interpreting the Type Theory as a Category there or synonymously, constructing a category from your type theory. But the notion of an 'algebra' is still too far for me. As well, a sum of products is just a discriminated union so that doesnt bring the idea of an algebra much close on its own.

Quote:

An algebraic type is an initial algebra for an endofunctor. It has some construction operations and a fold to destruct it by structural recursion.

A coalgebraic type is a final coalgebra for an endofunctor. It has some destruction operations and an unfold to construct it by guarded corecursion.

This is the part I get as I stated in my last post. that algebraic types are constructed/interpretable in terms of an F-Algebra.

So that must mean the term's origin was motivated by categorical concepts?

Quote:Original post by Daerax
Yeah but you're interpreting the Type Theory as a Category there or synonymously, constructing a category from your type theory.

Well the way categorical semantics works is by interpreting types as objects and terms as morphisms of some category.

Quote:So that must mean the term's origin was motivated by categorical concepts?

I'm not sure.

I know that early versions of ML only had primitive sum and product types and you had to encode everything in terms of them.

Algebraic data types cropped up later, and I don't think they were initially called "algebraic data types". Maybe they were only given the name "algebraic" when category theory started having an influence on PLT and the connection to initial algebras was seen. The dual coalgebraic types were definitely pulled straight from category theory, along with monads.