For example all functions with Int -> Int are type equivalent, because structural equivalency is used. Most of the time the functions are not compatible because they have different pre/post conditions, even though they seem to have the same input output types. I rather make my functions an instance of a type-class to tell the compiler that they can be used interchangably. For example sqrt :: Float -> Float sqrt a = /* pre : a >= 0 */ negate :: Float -> Float /* no precondition */ are different functions. You cannot just plug one in place of another (you can in Haskell because of structural type equivalency). Also a function working over (Int,Int) will do so even if the numbers are totally irrelevant to that function. They maybe the number of (apples,oranges) or number of (books,authors). However, data D a b = MkD a b data E a b = MkE a b (D Int Int) and (E Int Int) are trated as different because of name equivalency testing. Basically there are 2 type constructors -> ( , ) with structural equivalency, which is odd. Someone just dumped some idiosyncracies of lamda calculus into the language. Thanks again.

Cagdas Ozgenc writes: | Greetings. | | I know 2 special type constructors(there might be other that I do | not know yet) -> and ( , ) where structural type equivalency is | enforced and we can also create new types with an algebric type | constructor notation where name equivalency is enforced. | | What is the rationale? I mean why 2 special type constructors, but | not 5, or 10 or N? | | Thanks for taking time.

-> and (,) are names of type contructors, each with kind *->*->*.

Offhand, I don't see any difference in the way we'd test equivalency involving -> or (,) or D, where:

data D a b = MkD a b

If that doesn't help, will you please give a more concrete example of what you mean?

Regards, Tom

I remain puzzled by the thrust of your argument however one bit did make sense:

Also a function working over (Int,Int) will do so even if the numbers are totally irrelevant to that function. They maybe the number of (apples,oranges) or number of (books,authors).

It sounds like you want dimension types. In their original form, dimension types were concerned with physical dimensions like metres and time and combinations like metres per second per second. As I understand it we've now progressed to the point where we can talk about functions which do things like taking values of type 'books per second' and 'books per author' and returning 'authors per second' (or something like that). Anyway, dimension types have been studied by Andrew Kennedy http://research.microsoft.com/users/akenn/ (and others) and can be encoded in HM(X) http://www.cs.mu.oz.au/~sulzmann/projects.html a very researchy extension of Haskell's type classes. -- Alastair Reid reid@cs.utah.edu http://www.cs.utah.edu/~reid/

Cagdas Ozgenc wrote:

...

From the previous discussion it has been brought to my attention that there is no much difference between

a -> b

and

data F a b = Blank a b -- "-> probably has a blank value constructor"

Therefore it should be trivial to define a label initialized to a function abstraction without using the -> type constructor. I mean

fun :: F Int Int fun ? = ?

now what do I write in place of 1st and 2nd question marks? Even if I can do this, how am I suppose to invoke fun so that it would yield an "Int" not a "F Int Int"?

The type constructor F and the type constructor (->) are quite different. They have the same kind, but just as the type only tell you part of what a value is, thekind only tells you part of what a type is. Very informally a value of type "F a b" means "I have an a and a b", whereas as type "a -> b" means "if you give me an a I'll give you a b". So the function arrow "consumes" its first argument rather than produces it.

Or maybe I should ask the following question: what would the "value constructor" of -> look like, theoretically?

Well, in Haskell it looks like "\ x -> e". It different from data type constructors in that it's a binding construct, but it's the thing that constructs objects in a function type. -- Lennart

Cagdas Ozgenc wrote:

Then either -> is not a type constructor, or the concept of type constructors has to be divided into two : consuming type constructors, and producing type constructors. If so then language has to support a way to define consuming type constructors as well, in order to be consistent within itself.

I think -> is defined to be a type constructor to make functions first class values. In the meantime, type systems that support subtyping seem to treat the arrow in a special fashion. For example

if A <: B and C <: D then (B -> C) <: (A -> D) where a <: b indicates 'a' being a subtype of 'b'

A language with subtyping would have to treat any contravariant type constructors in a similar way. -- Lennart