Revamping the numeric classes

[Tom Pledger]

Marcin 'Qrczak' Kowalczyk writes:
 | On Thu, 8 Feb 2001, Tom Pledger wrote:
 | 
 | > nice answer: give the numeric literal 10 the range type 10..10, which
 | > is defined implicitly and is a subtype of both -128..127 (Int8) and
 | > 0..255 (Word8).
 | 
 | What are the inferred types for
 |     f = map (\x -> x+10)
 |     g l = l ++ f l
 | ? I hope I can use them as [Int] -> [Int].

f, g :: (Subtype a b, Subtype 10..10 b, Num b) => [a] -> [b]
Yes, because of the substitution {Int/a, Int/b}.

 | >         x + y + z                 -- as above
 | > 
 | >     --> (x + y) + z               -- left-associativity of (+)
 | > 
 | >     --> realToFrac (x + y) + z    -- injection (or treating up) done
 | >                                   -- conservatively, i.e. only where needed
 | 
 | What does it mean "where needed"? Type inference does not proceed
 | inside-out.

In the expression

    (x + y) + z

we know from the explicit type signature (in your question that I was
responding to) that x,y::Int and z::Double.  Type inference does not
need to treat x or y up, because it can take the first (+) to be Int
addition.  However, it must treat the result (x + y) up to the most
specific supertype which can be added to a Double.

 | What about this?
 |     h f = f (1::Int) == (2::Int)
 | Can I apply f

h?

 | to a function of type Int->Double?

Yes.

 | If no, then it's a pity, because I could inline it (the comparison
 | would be done on Doubles).  If yes, then what is the inferred type
 | for h? Note that Int->Double is not a subtype of Int->Int, so if h
 | :: (Int->Int)->Bool, then I can't imagine how h can be applied to
 | something :: Int->Double.

There's no explicit type signature for the result of applying f to
(1::Int), so...

h :: (Subtype a b, Subtype Int b, Eq b) => (Int -> a) -> Bool

That can be inferred by following the structure of the term.  Function
terms do seem prone to an accumulation of deferred subtype
constraints.

Regards,
Tom