Haskell: Is it possible to use numbers as data constructors?

Question

I have some data, and I want to test, what is the best way to store them. I am deciding between binary, quad, octal and hexadecimal data types.

The only way to check which is the best, is to use each of them in my algorithm and then see the results.

So far my implementation looks like this:

{-# LANGUAGE DeriveAnyClass #-}

data Binary = O | I         
              deriving (Bounded, Enum, Eq, Ord, Show)
data Octal  = OA | OB | OC | OD | OE | OF | OG | OH 
              deriving ( ... )

But I would like more general constructors like data Binary = 0 | 1. Is it possible to do that?

Answer 1

It's not possible to get the exact syntax you want, but there are ways to generically define a "between 0 and n" type in a way that they share constructors, and then use numeric literals as abstract constructors.

The finite-typelits package offers a type parameterized over the number of elements it has, so:

x :: Finite 4

would be a type with four inhabitants: 0, 1, 2, and 3. If you ever have a value of type Finite 4, you can be sure that it is one of those four values (or something silly like undefined or some other bottom). You can't pattern match on it directly, but you can project a Finite 4 into the integers by using getFinite :: Finite n -> Integer.

So in this scheme, you'd have:

type Binary = Finite 2
type Quad   = Finite 4
type Octal  = Finite 8

You can can indirectly pattern match:

processBinary :: Binary -> String
processBinary d = case getFinite d of
    0 -> "It's a zero"
    1 -> "it's a one"
    _ -> -- this case should be impossible, even though the compiler can't verify that.

And, you can even "construct" them using numeric literals using their (partial) Num instance:

> putStrLn (processBinary 0)
It's a zero
> putStrLn (processBinary 0)
It's a one

So this might be the closest thing to what you want! But there are a couple of drawbacks -- the compiler can't verify that your pattern matching statements are complete, and it also can't verify that your numeric literals are actually valid and won't be out of range for the type you're using.

> putStrLn (processBinary 2)
** Error: Runtime error!  Sucks :'(

There's also the convenient weakenN and strengthenN functions, which allow you to use a Finite 2 as if it were a Finite 8 (use a Binary digit as if it were an Octal digit), and also to use a Finite 8 as if it were a Maybe (Finite 2).

binDigitToOctalDigit :: Binary -> Octal   -- Finite 2 -> Finite 8
binDigitToOctalDigit = weakenN

---

There's another method that doesn't match what you want exactly, but there are some advantages. What you can do is have an recursive/inductively defined defined type (like lists) that are "constructed" to only have so many constructors, parameterized again on some type-level numeral. type-combinators offers one such type. There, you'd have:

type Binary = Fin (S (S Z))     -- "2"
type Octal  = Fin (S (S (S (S (S (S (S (S Z))))))))   -- "8"

The library does offer convenient type synonyms, so you could instead write:

type Binary = Fin N2
type Quad   = Fin N4
type Octal  = Fin N8

and the Fin type is constructed to have exactly the number of constructors indicated by the type. Fin N2 has two constructors:

1. FZ :: Fin N2
2. FS FZ :: Fin N2

And Fin N8 has eight constructors, FZ, FS FZ, FS (FS FZ), etc.

Fin has a projection function as well, fin :: Fin n -> Int, so you can use it the same way as you'd use Finite, and pattern match on an Int literal. But! The advantage of having this is that you can also directly pattern match on the constructors, and the compiler will ensure completeness:

processBinary :: Fin N2 -> String
processBinary d = case d of
  FZ    -> "It's a zero"
  FS FZ -> "It's a one"

And GHC can actually verify that you've handled every option :)

And, you also can't ever accidentally use a constructor that's "out of range":

> putStrLn (processBinary FZ)
It's a zero
> putStrLn (processBinary (FS (FS FZ))
-- that is a compile error!  neat, the compiler would tell you that this isn't allowed!

The library defines weaken similar to how the finite-typelits library does. It doesn't define strengthen, but it's possible to implement it if you need it :)

binDigitToQuadDigit :: Binary -> Quad      -- Fin N2 -> Fin N4
binDigitToQuadDigit = weaken . weaken