Blindness.hs

-- Everything down below is in Idris pseudocode

data EvenOrOdd : (n : Int) -> Type where
  Even : {n : Int} -> (k : Int) -> (2 * k = n)     -> EvenOrOdd n
  Odd  : {n : Int} -> (k : Int) -> (2 * k + 1 = n) -> EvenOrOdd n
  
-- let's drop all computational information
data EvenOrOdd = Even | Odd

-- let's drop all names (except type alias)
-- not sure if it is valid syntactically...
type EvenOrOdd = Either (n : Int, k : Int, 2 * k = n) (n : Int, k : Int, 2 * k + 1 = n)

-- let's drop computational information in the odd case
data EvenOrOdd : (n : Int) -> Type where
  Even : {n : Int} -> (k : Int) -> (2 * k = n)     -> EvenOrOdd n
  Odd  : EvenOrOdd n -- n is automatically implicit here
  
-- and the proof
data EvenOrOdd : Type where
  Even : Int -> EvenOrOdd
  Odd  : EvenOrOdd

-- and the names (except type alias)
type EvenOrOdd = Option Int

-- and the value
type EvenOrOdd = Boolean

-- and finally let's drop the distinction between even and odd integers...
type EvenOrOdd = Unit
-- ;)

-----------------------------------------------------------------------------

-- A slight re-interpretation of the original idea (isomorphic to the original type).
data EvenOrOdd : (n : Int) -> Type where
  Even : {n : Int} -> (k : Int) -> (2 * k = n)           -> EvenOrOdd n
  Odd  : {n : Int} -> ((k : Int) -> (2 * k = n) -> Void) -> EvenOrOdd n