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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
