Dan Weston wrote:
Questioning apfelmus definitely gives me pause, but...
Don't hesitate! :) Personally, I question everyone and everything, including myself. This is a marvelous protection against unintentionally believing things just because I've heard them several times like "Monads are hard" or "Haskell code is easier to understand", but has many more uses. As Feynman put it: "What do you care what other people think?"
id :: a -> a -- "arity" 1 id = ($) :: (a -> b) -> (a -> b) -- "arity" 2
I agree with the arities given above (but without quotes) and see no ill-definedness to arity.
But these are two different classes of functions. There are arguments of the first function that cannot be applied to the second (e.g. 5).
The fact that the two have different type signatures shows that Haskell can distinguish them (e.g. in the instantiation of a type class).
No, I think not. Having different type signatures is not enough for being distinguishable by type classes. The second type ∀a,b. (a -> b) -> a -> b is an instance of the first one ∀a. a -> a "Instance" not in the sense of class instance but in the sense of type instance, i.e. that we can obtain the former by substituting type variables in the latter, here a := (a -> b). Formally, we can write this as an "inequality" ∀a. (a -> a) < (a -> b) -> a -> b with "x < y" meaning "x less specific than y" or "x more general than y". Now, the property I meant with
I don't like this behavior of wrap since it violates the nice property of polymorphic expressions that it's unimportant when a type variable is instantiated is that the class instance predicate is monotonic with respect to the type instance relation: from x < y and Num x , we can always conclude Num y . In particular, let's examine a type class
class Nat a => Arity a f | f -> a describing that the function type f has a certain arity a which is expressed with Peano numbers in the type system: data Zero = Zero data Succ a = Succ a type One = Succ Zero type Two = Succ One class Nat n instance Nat Zero instance Nat n => Nat (Succ n) Now, if Arity One (∀a . a -> a) is true then due to monotonicity, Arity One ((a -> b) -> a -> b) must be true, too! The only possible solution to this dilemma is to drop the class instance for (∀a. a -> a). It's no problem to have many special instances Arity One (Int -> Int) Arity One (Char -> Char) etc. but we can't have the polymorphic one. In other words, not every (potentially polymorphic) function type has a well-defined arity! Oleg's hack basically supplies all those possible particular instances while avoiding the polymorphic one. Concerning the ill-definedness of wrap id
:type wrap id wrap id :: (FunWrap (a -> a) y) => [String] -> y
but trying to use it like in
let x = wrap id ["1"] :: Int
yields lots of type errors. We have to specialize the type of id before supplying it to wrap . For example,
wrap (id :: Int -> Int)
works just fine.
which I don't like, it seems that I have to life with it. That's because the toy implementation class FunWrap f x | f -> x where wrap :: f -> [String] -> x instance FunWrap (Int -> Int) Int where wrap f [x] = f (read x) instance FunWrap ((Int -> Int) -> Int -> Int) Int where wrap f [g,x] = f id (read x) already shows the same behavior. When trying something like
wrap id ["1"] :: Int
, GHCi complains that there's no polymorphic instance FunWrap (a -> a) Int There can't be, since that would disallow the special instances and moreover conflict with the functional dependency. So, wrap id is an example of an essentially ill-typed expression that the type checker does not reject early (namely when asking for its type). Regards, apfelmus