Encoding even integers using integers.

Evens.hs

{-

bryanwoods: Haskell folk: Any way to type a function like
generateEvens = [x | x <- [1..], x `mod` 2 == 0]
such that it always returns even numbers?

pedrofurla: @bryanwoods @puffnfresh in ghci `let generateEvens = ...` compiled just fine here

bryanwoods: @pedrofurla I was wondering if I could write a type signature like: generateEvens :: [EvenNumber]

techtangents: @justinleitgeb @bryanwoods @pedrofurla you can encode an even number type without dependent types.

bryanwoods: @techtangents @justinleitgeb @pedrofurla  Could you share an example?


techtangents:

Well, the sets of 'natural numbers' and 'even natural numbers' are of the same size - aleph-naught. 
They are both 'countably infinite' sets. 

From wikipedia:
'aleph-naught is the cardinality of the set of all natural numbers, and is the first infinite cardinal, 
called ω or ω0. A set has cardinality aleph-naught if and only if it is countably infinite, which is the 
case if and only if it can be put into a direct bijection, or "one-to-one correspondence", with the 
natural numbers. Such sets include the set of all prime numbers, the set of all integers, the set of 
all rational numbers, the set of algebraic numbers, the set of binary strings of all finite lengths, 
and the set of all finite subsets of any countably infinite set.'

There is a one-to-one correspondence between natural numbers and even natural numbers. i.e.
Natural : 0 1 3 4
Even    : 0 2 6 8

No matter how high you go, there will always be a natural number you can match up with an even number.

We can use this property to encode the even numbers. We will model an even number as a natural number 
half its value. When converting, we halve on the way in, and double on the way out. 

I'm going to use the Integer type as the base type, as this encoding also works for negative integers. 
Also, because Integer is unbounded.

-}

import Control.Applicative ((<$>))

data EvenNumber = EvenNumber Integer

instance Show EvenNumber where
  show = show . evenToInteger

evenToInteger :: EvenNumber -> Integer
evenToInteger (EvenNumber x) = x * 2

integerToEven :: Integer -> Maybe EvenNumber
integerToEven x = if (x `mod` 2 == 0) then (Just . EvenNumber $ x `div` 2) else Nothing

double :: Integer -> EvenNumber
double = EvenNumber

halve :: EvenNumber -> Integer
halve (EvenNumber x) = x 

evens :: [EvenNumber]
evens = double <$> [1..]

{-

λ integerToEven 6
Just 6

λ integerToEven 3
Nothing

λ double 3
6

λ halve (double 3)
3

λ evenToInteger (double 3)
6

λ take 5 evens
[2,4,6,8,10]


-}

The 'halve' function is interesting. Halving any integer ('normal' division, not integer division ("div")) yields a rational, not an integer. However, since we have a type that enforces evenness, halving an EvenNumber always yields an Integer.