[Haskell-cafe] Re: distinguish functions from non-functions in a class/instances

[apfelmus]

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