Hacker News Reader

Comment by throwaway17_17 | Hacker News Reader

Can you expand on what you mean by calling Haskell’s type system ‘ad hoc’? I was under the impression that ‘ad hoc’ was basically the opposite of formalized/well-founded. That doesn’t sound like an accurate description of Haskell’s type system in my understanding.

View on HN

For example, aptly named ad hoc polymorphism and overloading violates referential transparency:

    ( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )

This yields:

    (True,False)

suggesting that the same arithmetic expression is both 1 and 0. Yet, the ability to plug in expressions and reason algebraically about their values was frequently advertised as a core property of Haskell. This example shows that we cannot do this in general, we must also take into account the types, which in this case seem to be defined in a rather "ad hoc" way, by reflecting low-level implementation details such as the range of admissible integers in the type system.

In GHC, there is a dedicated flag to spot such cases (-fwarn-type-defaults).

In general, the guarentees that the type system actually gives and also the ways to specify them appear somewhat unfinished and are also quite hard to understand, often necessitating semantic restrictions and syntactic extensions. For further examples, see for instance:

https://stackoverflow.com/questions/27019906/type-inference-...

https://stackoverflow.com/questions/14865734/referential-tra...

For readers wondering why this is, there are a few things at play here. I preface my explanation by saying that the benefit of type classes vastly outweigh issues like the above example. Also if I put the above example in my work project I immediately get a warning about the exact issue, so it's not like it is a foot gun or anything like that. Anyhow:

0. Integer is arbitrary precision while Int is bounded, machine dependent (eg. 32 or 64 bit). They are both instances of the Num type class as well as the Integral type class as we'll see later.

1. Numbers without explicit type signatures are overloaded (aka. constraint polymorphic):

  λ> :t 1
  1 :: Num p => p

where p can be any type that has a Num constraint, like Integer or Int.

2. As per https://www.haskell.org/onlinereport/decls.html#sect4.3.4 we have

  default (Integer, Double)

as concrete types for numbers to default to in expressions without explicit type signatures to guide inference.

3. The type of the list index operator is:

  λ> :t (!!)
  (!!) :: [a] -> Int -> a

where the index is a concrete Int type.

Right, so in the above example if we check the type of 7^7^7`mod`5`mod`2

  λ> :t 7^7^7`mod`5`mod`2
  (7^7^7`mod`5`mod`2) :: Integral a => a

it is still overloaded (Integral), ie. can be either Integer or Int. Now in the first case there's nothing to concretise the type thus we are defaulting to Integer as per the defaulting rule. In the second case the usage of (!!) concretise the type to an Int. As 7^7^7 is big it does not fit in an Int (overflows). Compare:

  λ> 7^7^7`mod`5 :: Integer
  3
  λ> 7^7^7`mod`5 :: Int
  2

The mystery is now solved. Side note: if we do

  default ()

to prevent GHC defaulting we'll get a type error and we will be forced to specific a type. We can also say:

  λ> ( (7^7^7`mod`5`mod`2)==1, [False,True]!!fromInteger((7^7^7`mod`5`mod`2)) )
  (True,True)

In the context of Haskell "ad-hoc" means ad-hoc polymorphism.

See https://wiki.haskell.org/Polymorphism for details on parametric (ie. unconstrained) vs. ad-hoc (ie. constrained) polymorphism. In short the difference is that ad-hoc is parametric + one or more type class constraints. Eg. in:

  λ> :t fmap
  fmap :: Functor f => (a -> b) -> f a -> f b

the type variables a and b are unconstrained while f is constrained by the Functor type class.

Reply on news.ycombinator.com