11
votes

I want to define what seems to require an infinite type.

Required : a function "eat" that eats all it's arguments except "3" for which it returns 3

eat 3 = 3
eat x = eat

So basically an arbitrary expression like "eat (+) foldl (Just 5) 3" evaluates to 3. But the problem here is the type of eat. What should that be?

The closest i got to a running code was :

newtype Rec = MakeRec (Int -> Rec)

eat :: Int -> Rec
eat x = MakeRec eat


instance Show Rec where
     show _ = "EAT"

This works okay for "eat 6" but not for "eat 6 7" and it doesn't work if i put (eat 3 = 3) in it's definition.

I am not sure if this is even possible in Haskell. (What argument would one use to show it's not possible ?)

UPDATE : As noted in solution below, the type-information is needed at compile time so that compiler can know if "eat foldl 3 foldl" is invalid or not. So, exact solution to this problem is not possible.

1

1 Answers

23
votes

It's not possible. Infinite types (that aren't data types) are explicitly forbidden in Haskell, and it's easy to produce code which would require them, and thus produces an error (for example, try let foo = (42, foo) in foo).

You can, of course, create them with newtype and data, like you did, but then you have to explicitly wrap and unwrap the values in and out of constructors.

This is an explicit design decision: with infinite types, many obviously wrong expressions that we would like the compiler to reject would have to be allowed, and since many more programs would be allowed, a lot of previously unambiguously-typed programs would become ambiguously typed,1 requiring explicit type annotations. So a tradeoff is made: requiring you to be explicit about the fairly rare uses of infinite types in return for getting much more help from the type system than we otherwise would.

That said, there is a way to define something similar to your eat function, using typeclasses, but it can't stop only when you give it a 3: whether you've given it a 3 or not can only be determined at runtime, and types are decided at compile time. However, here's an overloaded value that can be both an Integer, and a function that just eats up its argument:

class Eat a where
    eat :: a

instance Eat Integer where
    eat = 3

instance (Eat r) => Eat (a -> r) where
    eat _ = eat

The catch is that you need to specify the types precisely when you use it:

*Main> eat 1 foldr ()

<interactive>:6:1:
    Ambiguous type variable `t0' in the constraint:
      (Eat t0) arising from a use of `eat'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: eat 1 foldr ()
    In an equation for `it': it = eat 1 foldr ()
*Main> eat 1 foldr () :: Integer
3

This is because eat 1 foldr () could be an Integer, but it could also be another function, just as we used eat 1 and eat 1 foldr as functions in the same expression. Again, we get flexible typing, but have to explicitly specify the types we want in return.

1 Think typeclass overloading, like the overloaded numeric literals (42 can be any type that's an instance of Num).