Can the semantics of a numeric hierarchy be faithfully represented in Haskell?

Question

I am trying to represent a fragment of a number hierarchy using the Haskell concepts of value, type, and type class. I would like the Haskell code to reflect the mathematical semantics $\vdash ((x \in \mathbb{N}) \land (\mathbb{N} \subset \mathbb{Z}\subset \mathbb{Q}) \Rightarrow (x \in \mathbb{Q}))$. In words, given that the set $\mathbb{N}$ of natural numbers is a subset of the the set $\mathbb{Z}$ of integers and integers are a subset of rationals $\mathbb{Q}$, we can deduce that every natural number is an rational number. I omit the constraint that natural numbers are actually a proper subset of integers.

Below is my attempt at relating the math and Haskell semantics. I am unsure whether a class is a set of types as stated by GAST (Section 3.5) and hence a type can be considered as an element of a class $(T \in TC)$.

Note it is possible that $V_1=V_2$ (e.g. 1:Nat=1:Int)

Below is my flawed attempt to capture the mathematical meaning using Haskell. I am aware that implementing rationals would lead to a situation where rationals were represented by both a type and a type class (not good!). Please note for research purposes I am restricted to only using values, types,and type class. I am not intentionally seeking to impose Object Oriented class semantic on Haskell.

data Natural = One | Suc Natural deriving Show
data Integers = Zero | Succ Integers deriving Show

class RationallNumbers x where
  plus::x -> x -> x

instance RationallNumbers Integers where 
 plus  x  Zero = x
 plus  x  (Succ y)  = Succ (plus x  y)

instance RationallNumbers Natural where
 plus  x  One = Suc x
 plus  x  (Suc y)  = Suc (plus x  y) 

twoPlusTwoNat = plus (Suc One)  (Suc One)
twoPlusTwoInt = plus (Succ (Succ Zero))  (Succ (Succ Zero))

To sum up my question is:

Can the numeric hierarchy described be represented in Haskell using the semantic concepts of values, types, and classes?

Related questions: A mathematical (categorical) description of type classes, Is there a model theory for Haskell type classes?

Answer 1

Yes, it is definitely possible. However your approach is a good starter but keep in mind to have a functional approach on writing code in Haskell. You can create expressions so you can define and 'override' methods.

As a suggestion I will give a part of code of how such expressions can look like as values and types.

data Exp = Lit Value
         | Assign Name Exp
         | Variable Name
         | Apply Exp Exp
         | Assist Name Exp
         | Exp :+:  Exp
         | Exp :-:  Exp
         | Exp :*:  Exp
         | Exp :=:  Exp
         | Exp :==: Exp
         | Exp :/=: Exp
         | Exp :>:  Exp
         | Exp :>=: Exp
         | Exp :<:  Exp
         | Exp :<=: Exp
         | Exp :&&: Exp
         | Exp :||: Exp
         deriving (Show)

This is some code out of a language I've written for controlling micro-controllers. The evaluation can be done as following:

-------------------------------------------------
-- Evaluate Expressions Utilities
-------------------------------------------------
-- Evaluate Integer Arithmetic operations
evalInt :: KDLMap -> Exp -> Int
evalInt _ (Lit n)          =  kdlintToInt n
evalInt k (Variable n)     =  kdlintToInt $ searchVariable' n k
evalInt k (e :+: f)        =  evalInt k e + evalInt k f
evalInt k (e :*: f)        =  evalInt k e * evalInt k f
evalInt k (e :-: f)        =  evalInt k e - evalInt k f
evalInt _ _                =  Prelude.error "Unable to perform operation."

-- Evaluate Boolean operations with Integers
evalIntBool :: KDLMap -> Exp -> Bool
evalIntBool k (e :<:   f)         =  evalInt k e <  evalInt k f
evalIntBool k (e :>:   f)         =  evalInt k e >  evalInt k f
evalIntBool k (e :<=:  f)         =  evalInt k e <= evalInt k f
evalIntBool k (e :>=:  f)         =  evalInt k e >= evalInt k f
evalIntBool k (e :/=:  f)         =  evalInt k e /= evalInt k f
evalIntBool k (e :==:  f)         =  evalInt k e == evalInt k f
evalIntBool _ _            =  Prelude.error "Unable to perform operation."

-- Evaluate Boolean operations with Booleans
evalBool :: KDLMap -> Exp -> Bool
evalBool _ (Lit n)         =  kdlboolToBool n
evalBool k (Variable n)    =  kdlboolToBool $ searchVariable' n k
evalBool k (e :&&: f)      =  evalBool k e && evalBool k f
evalBool k (e :||: f)      =  evalBool k e || evalBool k f
evalBool _  _              =  Prelude.error "Unable to perform operation."

For more information, hit me up. I will provide it on my github quite soon, so you can see more. But to answer your question, yes it's definitely possible.