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

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?

• link thanks for your solution which I am certain will work. But, I am more concerned with the actual semantics of Haskell types and classes in implementing a hierarchy. – Patrick Browne Nov 24 '17 at 15:18
• I am quite familiar with Haskell, but I can't really understand your question. You use $\mathbb Z$ as both a type and a type class, which puzzles me -- even if you say you are aware of that. Perhaps you want subtypes, which Haskell does not have. Usually, without subtypes, you use "inclusion" functions to move from $\mathbb N$ to $\mathbb Z$, so that they can be separate types, but you can still inject the first into the latter when needed. – chi Nov 24 '17 at 21:03
• chi is of course correct to point out the strange representation of Integers as both data and class. This is represents my confusion about type classes. Although there is a relation values-to-types and a relation types-to-classes, there is no transitive relation from value-to-class. In short a value can never be an element of a type class i.e. $V \notin TC$. – Patrick Browne Nov 25 '17 at 9:19
• I believe that the two solution proposed "inclusion" and "expressions" will allow $\mathbb{Z}$ and $\mathbb{N}$ to be implemented. But without some form of sub-typing it is hard to see how those implementations would satisfy the mathematical semantics. – Patrick Browne Nov 25 '17 at 9:20
• chi I have updated the question based on your comments. – Patrick Browne Nov 25 '17 at 10:15

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.