5
$\begingroup$

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)$.

Math and Haskell Semantics 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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Patrick Browne Nov 24 '17 at 15:18
  • 1
    $\begingroup$ 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. $\endgroup$ – chi Nov 24 '17 at 21:03
  • $\begingroup$ 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$. $\endgroup$ – Patrick Browne Nov 25 '17 at 9:19
  • $\begingroup$ 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. $\endgroup$ – Patrick Browne Nov 25 '17 at 9:20
  • $\begingroup$ chi I have updated the question based on your comments. $\endgroup$ – Patrick Browne Nov 25 '17 at 10:15
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.