{-# LANGUAGE DeriveDataTypeable, NoMonomorphismRestriction #-}

import Data.Typeable
import Prelude hiding (elem)

data Set = Set { contains :: (Typeable a) => a -> Bool } deriving (Typeable)

elem = flip contains

f x = case (cast x) of
Just a -> not (x `elem` a)
Nothing -> False

self = Set f

paradox = self `elem` self

Evaluating this in Haskell produces an infinite loop, which is not an inhabitant of Bool. The error lies in the implementation of cast. It should detect the recursion, returning Nothing, and thus make paradox = False.

Deriving a formal semantics for cast would be an interesting project; any takers?

Advertisements