naive type checking II (not so naive?) 
Author Message
 naive type checking II (not so naive?)

I have a question that is prompted by, but tangential to Greg
Michaelson's request about naive type-checking.  It is probably
Haskell/Hugs specific.

Hoping to demonstrate to my class the advantages of always declaring the
types of functions, I came up with the following simple erroneous
script:

Quote:
> myEven   :: Int -> Bool
> myEven x  = x `div` 2

I expected an error to be reported that the type of myEven was
Integral a => a -> a  but Hugs gave me:

ERROR "test.lhs" (line 12): Type error in function binding
*** term           : myEven
*** type           : Bool -> Bool
*** does not match : Int -> Bool

How does it come up with Bool -> Bool?  I expected myEven to be typed
and then that type compared with the declaration.  I can't see how any
substitution into  Integral a => a -> a  gives  Bool -> Bool.

I guess this is tied up with classes and instances because Gofer gives:

ERROR "test.lgs" (line 12): Type error in function binding
*** term           : myEven
*** type           : Int -> Int
*** does not match : Int -> Bool

Any explanations?

Clem Baker-Finch
--



Mon, 16 Aug 1999 03:00:00 GMT  
 naive type checking II (not so naive?)

[...]

Quote:
> > myEven   :: Int -> Bool
> > myEven x  = x `div` 2

> I expected an error to be reported that the type of myEven was
> Integral a => a -> a  but Hugs gave me:

> ERROR "test.lhs" (line 12): Type error in function binding
> *** term           : myEven
> *** type           : Bool -> Bool
> *** does not match : Int -> Bool

> How does it come up with Bool -> Bool?  I expected myEven to be typed
> and then that type compared with the declaration.  I can't see how any
> substitution into  Integral a => a -> a  gives  Bool -> Bool.

I don't really see it either, though I have a rough idea.
Type assertions on top level in Haskell (and in Miranda,
and probably in Gofer as well) have a greater significance
than one might think.  The problem is:

- the entire program/module is treated as a single letrec,
  there is no linear visibility as in SML
- as a result, the ML-typing technique for letrec would be
  useless, you couldn't use functions polymorphically
  within your module
- to remedy that, Haskell etc. make a dependency
  analysis on the call-graph and stratify the program
  into nested letrec's; roughly: if f calls g but g doesn't
  call f then we type-check g first and are able to use
  it polymorphically within the definition of f.
- moreover, whenever there is a type assertion for f one can
  ignore all the calls within its definition
  when making the dependency analysis; the type-checker simply
  uses the assertion when checking the rest of the program and
  finally has to check that the assertion is sound w.r.t. the
  definition of f.

The last point makes Haskell type inference more powerful than ML's,
because it also allows to use a function polymorphically within its
own definition.  Notice that Haskell type inference proceeds
differently: it doesn't first type-check and then compares with the
declaration, it uses the type assertion for the type-check.
[BTW Besides the additional expressive power this different technique
makes it easier for the user to find the actual culprit in an
ill-typed program, simply by adding type assertions; in SML this
doesn't really help.]

I guess, what happened was that Hugs took the type assertion Int->Bool
and exploited it in the left-hand side, getting Bool as the type
of the lhs, assumed therefore that x 'div' 2 was Bool as well
and then somehow concluded that therefore x was Bool.  Hmmmmmmmmmmm
Perhaps there is some funny overloading of 'div',
making the typing Bool->Bool of your definition possible???



Sun, 22 Aug 1999 03:00:00 GMT  
 naive type checking II (not so naive?)

 | > > myEven   :: Int -> Bool
 | > > myEven x  = x `div` 2

The thing is that the function `div' has the following type:

  -- Hugs
  div :: Integral a => a -> a -> a

  -- Gofer
  div :: Int -> Int -> Int

So, div doesn't check if a number is dividable by another number, it
_divides_ the number (truncating the result). Your function should
not use the function `div' at all. It should be something like:

  myEven   :: Int -> Bool
  myEven x  = x `rem` 2 == 0

About the different results of Hugs and Gofer.

-- Hugs

Hugs derives that the result of x `div` 2 is a Bool (as you stated).
Therefore x must also be of type Bool, since div :: a -> a -> a. But that
doesn't match with your type declaration. Error.

-- Gofer

Gofer derives that x and 2 are Int's, and therefore x `div` 2 is an
Int. This doesn't match with your declaration. Error.

Hope this helps,
Koen.

--

|                   http://www.cse.ogi.edu/~kcclaess/  |
|------------------------------------------------------|
|  Visiting student at OGI,    Portland, Oregon, USA.  |



Thu, 26 Aug 1999 03:00:00 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Naive polymorphic type checking - please help

2. comp.lang.apl access for the net-naive

3. Questions from a naive user

4. Questions from a naive st programmer

5. naive bayes classifier

6. Naive Forth questions

7. Extremely naive (and probably stupid) question

8. (Yet another) naive question

9. Naive question

10. Naive question

11. Another naive question

12. Naive Number Question

 

 
Powered by phpBB® Forum Software