HASKELL PROOFS

REVISED: Thursday, February 8, 2024

Haskell Proofs.

1. HASKELL TYPE THEORY

Propositions are types. A type corresponds to a theorem if that type is inhabited. Every type is inhabited by the value undefined in Haskell.

Prelude>  :type undefined

undefined :: a

Prelude>  

If we work with a limited subset of Haskell's type system, and disallow polymorphic types, we have a consistent logic system. Hereafter it is assumed we are working in such a type system.

2.  LAWS

Law of detachment called modus ponens or MP says if X is true then Y is true. X is true. Therefore Y is true. (A tautology is any sentence that must always be true.)

Law of the excluded middle says that every statement must be either true or false, never both or none.

3.  DEFINITIONS

3.1. ALGORITHM

An algorithm is a step-by-step procedure or formula for calculations, problem-solving operations, or accomplishing a task in a certain number of steps.

3.2. ARGUMENT

An argument is an attempt to persuade someone of something, by giving reasons or evidence for accepting a particular conclusion.

3.3. AXIOMS

Assumptions are called axioms or postulates. They are basic truths we accept on faith to get a theory started.

3.4. CONJUNCTION "&&" AND

The Boolean "and".

Prelude>  :type (&&)
(&&) :: Bool -> Bool -> Bool
Prelude>  

If the first argument of a conjunction evaluates to False, then the conjunction evaluates to False; if the first argument evaluates to True, then the conjunction gets the same value as its second argument.

Another way of expressing a conjunction is to find a value that contains two sub-values: the first whose type corresponds to A, and the second whose type corresponds to B; for example, a Haskell tupple (a, b).

3.5. CONTRAPOSITIVE PROOF 

If not q then not p.

3.6. CORROLARIES

When a theorem is proved, a few additional steps can produce one or more other theorems. Such a secondary theorem is called a corollary.

3.7. DEFINITION

A definition, an expression, is a well-defined and unambiguous unique interpretation or description of the essence of what is being defined.

Create a list of definitions, axioms, and postulates to use in your proof.

3.8. DIRECT PROOF 

If p then q.

p is the antecedent or hypothesis.

An antecedent is a preceding event, condition, or cause.

A hypothesis is a proposition made as a basis for reasoning, without any assumption of its truth.

q is the consequence. For example, the cause p results in the effect q. Therefore, q is the resulting consequence.

3.9. DISJUNCTION "||" OR

The Boolean "or".

Prelude>  :type (||)
(||) :: Bool -> Bool -> Bool
Prelude>  

If the first argument of a disjunction evaluates to False, then the disjunction gets the same value as its second argument. If the first argument of a disjunction evaluates to True, then the disjunction evaluates to True.

Another way of expressing a disjunction is to find a value which contains either a value of type A or a value of type B; for example, Haskell Either A B.

Prelude>  :type either
either :: (a -> c) -> (b -> c) -> Either a b -> c
Prelude>  

3.10. EQUIVALENCE ==

Logical equivalence is similar to Haskell equality ==.

Prelude>  :type (==)
(==) :: Eq a => a -> a -> Bool
Prelude>  

3.11. GIVEN

You start your proof with what is given.

A given or a supposition, is something that is accepted or assumed to be true without proof.

A postulate is a statement that is assumed true without proof.

3.12. HYPOTHESIS

The hypothesis is what you can assume is true at the beginning of the proof. Therefore, we begin a proof by listing the hypothesis.

3.13. IMPLICATION "IF THEN"

An expression of the form P => Q (if P, then Q; Q if P) is called the implication of P and Q. P is the antecedent of the implication and Q the consequent.

If we want to implement implication in Haskell, we can do so in terms of if, then, not, and ||.

The Boolean otherwise is defined as the value True.

The only time an implication is False is when the antecedent is True and the consequent is False.

3.14. INDUCTION

Recursive proofs are called induction. Mathematical Induction is a method of formal proof in which a statement is proved for one step in a process, and it is shown that if the statement holds for that step, it holds for the next. The beauty of induction is that it allows a theorem to be proven true where an infinite number of cases exist without exploring each case individually.

Step 1. Show that the statement is true for the initial value of n.

Step 2. Assume that the statement is true for n = k.

Step 3. Prove that the statement is true for n = k + 1.

Then it follows the statement must be true for all values of n.

3.15. LEMMAS

When the proof of a theorem involves many steps, it can help if we prove some preliminary theorems first, using them as stepping stones on the way to the final proof of the intended theorem. A minor theorem of this sort is called a lemma.

3.16. LOGICAL EQUIVALENCE

Logical equivalence is a type of relationship between two statements which translates verbally into "if and only if" and is symbolized by a double-lined, double arrow pointing to the left and right <=>.

3.17. MODUS PONENS

Modus ponens is a rule of inference which can be summarized as P implies Q and P is asserted to be true, so therefore Q must be true.

3.18. MODUS TOLLENS

Modus Tollens is the rule of logic stating that if a conditional statement ( if p then q ) is accepted, and the consequent does not hold ( not q ), then the negation of the antecedent ( not p ) can be inferred.

3.19. NEGATION "NOT"

A negation has the opposite truth value than that which is negated.

The Haskell equations f x y = ... used in the definition of a function f are genuine mathematical equations. They state that the left hand side and the right hand side of the equation have the same value.

Every statement that makes mathematical sense is either True or False.

Haskell uses True and False for the truth values. Together, these form the type Bool.

data means that we are defining a new data type. The part before the = denotes the type, which is Bool. The parts after the = are value constructors. They specify the different values that this type can have. The | is read as or. So we can read this as: the Bool type can have a value of True or False. Both the type name and the value constructors have to be capital cased.

data Bool = False | True

The Boolean "not".

Prelude>  :type not
not :: Bool -> Bool
Prelude>

Prelude>  not True
False
it :: Bool
Prelude>

Prelude>  not False
True
it :: Bool
Prelude>  

3.20. PROOF

A proof is a logical argument that establishes the truth of a statement. 

When building a proof, be sure that your argument is clearly developed and that each step is supported by a property, theorem, postulate or definition. 

3.21. PROOF BY CONTRADICTION 

Assume not p and find contradiction.

3.22. PROPOSITIONS

The process of theory-building involves taking the definitions and axioms and putting them together according to the rules of logic. Statements we intend to prove are called propositions until their truth has been firmly established. A proposition is a statement that is either True for False.

A sentence, also called a proposition, is the smallest possible entity in propositional logic.

A hypotheses, also called a proposition, is a supposition or proposed explanation made on the basis of limited evidence as a starting point for further investigation.

A conjecture, also called a proposition, is an idea believed to be true, but not yet proven. Conjecture is a statement or hypothesis, an educated and reasonable guess based on observed patterns.

The outcome, or logic value, of an operation in propositional logic is always either True or False.

A truth table is a method of denoting all possible combinations of truth values for the variables in a proposition. The values for the individual variables, with all possible permutations, are shown in vertical columns at the left. The truth values for compound sentences, as they are built up from the single-variable (or atomic) propositions, are shown in horizontal rows.

3.23. PROVE

To prove is to demonstrate or establish that something, a proposition, is True.

Order of operations:
1. Parentheses
2. Not
3. And, &&, left to right.
4. Or, ||, left to right.

Equational Reasoning:           
x + 0 = x   -- Identity for addition.
x * 1 = x    -- Identity for multiplication.
x + y = y + x   -- Commutative
x * y = y * x    -- Commutative 
(x + y) + z = x + (y + z)   -- Associative
(x * y) * z = x * (y * z)      -- Associative 
x * (y + z) = x * y + x * z   -- Multiplication distributes over addition.

Haskell QuickCheck:

QuickCheck is a tool for testing Haskell programs automatically. The programmer provides a specification of the program, in the form of properties which functions should satisfy, and QuickCheck then tests that the properties hold in a large number of randomly generated cases.

3.24. Q.E.D.

When mathematicians finish proofs, they write “Q.E.D.” at the end. This is an abbreviation of the Latin phrase, "Quod erat demonstradum". It translates as, “Which was to be demonstrated".

A □ tombstone symbol is also often used to signify the end of a proof.

3.25. REDUCTIO AD ABSURDUM

Reductio ad absurdum is a method of proving the falsity of a premise by showing that its logical consequence is absurd or contradictory.

3.26. SETS

There are a very large number of sets; common sets are as follows:

ℂ is the set of complex numbers; ℂ = {a number of the form a+bi where a and b are real numbers and i is the square root of -1.}.

ℝ is the set of real numbers; ℝ = {any positive or negative number; e.g., π, e, √2}.

ℚ is the set of rational numbers; ℚ = {ratio of two integers; e.g., 1/2}.

ℤ is the set of integers;  ℤ = {... -2, -1, 0, 1, 2, ...}.

ℕ is the set of natural numbers; ℕ = {1, 2, 3, 4, 5 ...}.

3.27. TAUTOLOGY

If you construct a truth table for a statement and all of the column values for the statement are true, then the statement is a tautology because it is always true.

3.28. THEOREMS

Once a proposition has been proved within the framework of a mathematical system, that proposition becomes a theorem. 

3.29. TRIVIALITY

A trivial solution is an easy obvious solution. For example:

0ⁿ + 0ⁿ + 0ⁿ = 0ⁿ

Despite the simplicity of the trivial case, it should not be ignored.

4. HASKELL 'PALINDROME' PROOF

4.1. GIVEN 

Hypothesis:

1. The character string "level".

2. Definition:

A palindrome is a word, phrase, or sequence that reads the same backward as forward.

4.2. TO BE PROVED 

Proposition:

The character string "level" is a palindrome.

4.3. PROOF

Algorithm:

Let s equal the character string "level". Reverse the string s. Compare the original string s to the reversed string. Return True if and only if s reads the same backward as forward.

Prelude>  let s = "level"
s :: [Char]
Prelude>

Prelude>  let ispal s = s == reverse s
ispal :: Eq a => [a] -> Bool
Prelude>

Prelude>  :type ispal
ispal :: Eq a => [a] -> Bool
Prelude>

Prelude>  ispal s

True

it :: Bool
Prelude>  

Q.E.D.

5. HASKELL 'FUNCTIONS ARE EQUAL' PROOF

5.1. EXAMPLE 1

5.1.1 GIVEN 

Hypothesis:

f x = ( 1 + x ) ^ 2

g x = x ^ 2 + 2 * x + 1

5.1.2. TO BE PROVED 

Proposition:

f x == g x

5.1.3. PROOF

Algorithm:

Prelude>  let f x = ( 1 + x ) ^ 2

f :: Num a => a -> a
Prelude>

Prelude> :type f

f :: Num a => a -> a

Prelude>  let g x = x ^ 2 + 2 * x + 1
g :: Num a => a -> a
Prelude>

Prelude>  :type g
g :: Num a => a -> a
Prelude>

Prelude> let x = 9  -- Substituting any integer value for x; f x == g x

x :: Num a => a
Prelude>

Prelude> f x == g x
True
it :: Bool
Prelude>

Prelude> import Test.QuickCheck

Prelude>

Prelude> let prop_fg x = f x == g x
prop_fg :: (Num a, Eq a) => a -> Bool
Prelude>

Prelude> quickCheck prop_fg
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()

Prelude>

Q.E.D.

5.2. EXAMPLE 2

5.2.1. GIVEN 

Hypothesis:

f x = ( x ^ 2 ) / x

g x = x

5.2.2 TO BE PROVED 

Proposition:

f x == g x

5.2.3. PROOF

Algorithm:

Prelude>  let f x = ( x ^ 2 ) / x

f :: Fractional a => a -> a
Prelude>

Prelude> :type f

f :: Fractional a => a -> a

Prelude>

Prelude>  let g x = x
g :: t -> t
Prelude>

Prelude>  :type g
g :: t -> t
Prelude>

Prelude> let x = 3  -- Substituting any integer value for x; f x == g x; EXCEPT FOR  0

x :: Num a => a
Prelude>

Prelude> f x == g x
True
it :: Bool
Prelude>

GHCi, version 9.8.1: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>

Prelude> import Test.QuickCheck
Prelude>

Prelude> let f x = (x^2) / x
f :: Fractional a => a -> a
Prelude>

Prelude> let g x = x
g :: t -> t
Prelude>

Prelude> let prop_fg x = f x == g x
prop_fg :: (Fractional a, Eq a) => a -> Bool
Prelude>

Prelude> quickCheck prop_fg
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
*** Failed! Falsifiable (after 1 test): 
0.0
it :: ()

Prelude>

The proof failed because of division by zero!

Substituting zero for x in g x = x is no problem.

Substituting zero for x in f x = (x^2) / x results in a division by zero error!

Prelude> f x == g x
True
it :: Bool
Prelude>

The above was misleading because it referred only to x = 3.

This is proof QuickCheck is a tool you should take the time to learn how to use.

6. CONCLUSION

In this tutorial, you have received an introduction to Haskell proofs.

7. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Doets K. & Van Eijck J. (2004). The Haskell Road to Logic, Maths  and Programming. Second Edition. Norcross, Georgia: College Publications, Inc.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL CATEGORY THEORY

REVISED: Wednesday, January 24, 2024

Haskell Category Theory.

I.  HASKELL "CATEGORY THEORY"

Category theory first appeared in a paper entitled "General Theory of Natural Equivalences", written by Samuel Eilenberg and Saunders Mac Lane in 1945.

The focus of category theory is on composition. A category is just a bunch of objects A, B, C... and some processes f, g, h...

There is one different identity process for each of the objects A, B, C... ; therefore, category theory is not polymorphic.

In set theory, morphisms are functions; however in category theory morphisms is a broadly similar idea, but somewhat more abstract: the mathematical objects involved need not be sets, and the relationship between them may be something more general than a map.

Category theory is a powerful tool for studying similarities. For example, generalizing set definitions for one-to-one and onto functions to category theory as shown below.

A. MONOMORPHISM

. read "of"; e.g, f of g, f.g is a function, such that (f.g)(x) = f(g(x)). The notation f o g means that we apply g first and then f.

Morphism is read "function".

A function f from A to B is called one-to-one if, whenever f (a) = f (b), then a = b.   No element of B is the image of more than one element in A.

In mathematics, an image is the subset of a function's codomain which is the output of the function on a subset of its domain. In other words, it can be thought of as a subobject, an object which sits inside another object in the same category. Therefore, a monic process defines a subobject.

What can go into a function is called the domain.

What may possibly come out of a function is called the codomain.

What actually comes out of a function is called the range.

For a one-to-one function f, for each g and h, if f.g = f.h then g = h and f is monic.

The monic process (monomorphism), also called a monic morphism or a mono, is a left-cancellative morphism. Which means a monic process can be canceled out on the left.

B. EPIMORPHISM

A function f from A to B is called onto if for all b in B there is an a in A such that f (a) = b.   All elements in B are used.

For an onto function f, for each g and h, if g.f = h.f then g = h and f is epic.

An epic process (epimorphism) is a right-cancellative morphism. Which means an epic process can be canceled out on the right.

C. ISOMORPHISM

: read "such that".

→ read "maps set" A into set B.

An iso process (isomorphism) is not an epic and monic process.

Let C be a category, and let X, Y be objects of C.

A morphism f:X→Y is an isomorphism if there exists a morphism g:Y→X such that:

g.f = id_X
f.g = id_Y

where id_X denotes the identity morphism on X.

II. INITIAL OBJECT

An initial object I is one from which there is one arrow from I to any other object. That kind of object is playing the role of the empty set. There is no initial object in the category of Haskell programs since any type is inhabited by undefined.

III. TERMINAL OBJECT

Given

∀ read "for every".
∈ read "is an element of".
• read "is a function of".
∃! read "there exists exactly one".
: read "such that".
→ read "maps set X into set T".

Then let C be a category.

A terminal object in C is an object T. T is playing a similar role to the singleton set.

T ∈ C :  ∀ X ∈ C ∃! morphism X → T

IV.  CATEGORY

A Category is a collection of objects and arrows. Arrows are called “morphisms” in Category Theory. An arrow points from a source object to a destination object. Arrows are relationships or functions. If you think of arrows as relationships an arrow could be a relationship like “greater than or equal”. If you think of arrows as functions, then the initial source object is the input to the function and the terminal output object is the output of the function.

V. CONCLUSION

In this tutorial, you have received an introduction to Haskell "Category Theory".

VI. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL MODULES DATA HIDING

REVISED: Monday, February 12, 2024

Haskell Data Hiding.

I. HASKELL DATA MODULES

You are reading "Haskell Modules Data Hiding", the second half of the "Haskell Data Modules" tutorial.

The first half is "Haskell Modules No Data Hiding".

The two parts of this tutorial are a very brief outline of "Haskell Programming Tutorial 6 - Modules" by Sankha Mukherjee. 

A. SKELETON

STEP 1: We start off with the following file containing the vector functions:

module MyVectorsF where

(·) :: (Float, Float, Float) -> (Float, Float, Float) -> Float
(·) (x1, x2, x3)(y1, y2, y3) =  x1*y1+x2*y2+x3*y3

(×) :: (Float, Float, Float) -> (Float, Float, Float) -> (Float, Float, Float)
(×) (x1, x2, x3)(y1, y2, y3) =  (x2*y3-x3*y2, x3*y1-x1*y3, x1*y2-x2*y1)

1. Create a new data type.

data Vec = V3DCart Float Float Float
        deriving (Show)

We use the data keyword to define a new data type. The part before the = denotes the data type, which is Vec. The parts after the = are value constructors. They specify the different values that this data type can have. V3DCart is a value constructor that has three fields, parameters, which take floats. Value constructors are actually functions that return a value of a data type. The value constructor V3DCart returns a value of data type Vec. Adding deriving (Show) at the end makes our Vec data type part of the Show type class so Haskell knows how to get the string representation of our value and then Haskell prints that out to the terminal. Value constructors are just functions that take the fields as parameters and return a value of some data type as a result. Not exporting the value constructors of a data type makes them more abstract in such a way that we hide their implementation. Also, whoever uses our module can not pattern match against the value constructors.

2. Create accessor function.

make3DCV :: Float -> Float -> Float -> Vec
make3DCV a b c = V3DCart a b c

Type constructors can take types as parameters to produce new types. The a b c shown above are type parameters. Because there are type parameters involved, we call make3DCV a type constructor. Type parameters are useful because we can make different types with them depending on what kind of types we want contained in our data type. If our data type acts as some kind of box container, as does Vec, it is good to use type parameters. The parts after the = are value constructors. Value constructors specify the different values that make3DCV can have. V3DCart is a value constructor that has three fields, a b c type parameters.  Value constructors are actually functions that return a value of a data type. The value constructor V3DCart returns a value of data type Vec. 

3. Create a new type class.

class VectorC a where
        (·) :: a -> a -> Float
        (×) :: a -> a -> a

We use the classs keyword to define a new type class, which is VectorC. Type classes are like interfaces. We do not make data from type classes. The a after VectorC is the data type variable and it means that a will play the role of the data type that we will soon be making when we make an instance of VectorC. It does not have to be called a, it does not even have to be one letter, it just has to be a lowercase word. Then, we define several functions; e.g., (·) and (×). It is not mandatory to implement the function bodies themselves, we just have to specify the type declarations for the functions. 

4. Create instances of the new type class.

instance VectorC  Vec where
        (·) (V3DCart x1 x2 x3) (V3DCart y1 y2 y3) = x1*y1+x2*y2+x3*y3
        (×) (V3DCart x1 x2 x3) (V3DCart y1 y2 y3) = (V3DCart (x2*y3-x3*y2) (x3*y1-x1*y3) (x1*y2-x2*y1))

We make an instance of VectorC by using the instance keyword. So class is for defining new type classes and instance is for making our data types instances of type classes. When we were defining VectorC,  we wrote class VectorC a where and we said that a plays the role of whichever data type will be made an instance later on. We can see that clearly here, because when we are making an instance, we write instance VectorC  Vec where. We replace the a with the actual data type Vec.

In summary, first, we  create a new data type Vec. Second, we create accessor functions make3DCV. Third, we think about what the Vec data type can act like and create type classes VectorC, that can behave in that way. Fourth, the functions of our new data type Vec,  are made instances of that type class VectorC. Notice, the behavior of type classes is achieved by defining functions or just type declarations that we then implement. When we say that a data type is an instance of a type class, we mean that we can use the functions (·) and (×), that the type class defines with that data type.

STEP 2: We start off with the following file containing the main function:

import MyVectorsF

main = do
    print $ (2,4,5) · (0,1,0)
    print $ (2,4,5) × (0,1,0)

1. Call imported accessor functions.

    let a = make3DCV 2 4 5

    let b = make3DCV 0 2 0

2. Print new output.

    print $ a · b

    print $ a × b

B. FLESH ON BONES

1. SAVE

Save has two steps. "Save Step 1" saves the vector functions. "Save Step 2" saves the main function.

SAVE STEP 1

Use your editor to save  MyVectorsF.hs which is the final draft of vector dot product, and cross product, function signatures and definitions:

module MyVectorsF (make3DCV, VectorC(..)) where   -- Export accessor functions and everything in the class.

class VectorC a where   -- Creates a new "type class" VectorC, which takes any generic data type a.
    (·) :: a -> a -> Float    -- Generic function signatures which take any data type a.
    (×) :: a -> a -> a

data Vec = V3DCart Float Float Float   -- Creates a new "data type" Vec.
    deriving (Show)

make3DCV :: Float -> Float -> Float -> Vec   -- Accessor function returns data type Vec.
make3DCV a b c = V3DCart a b c

instance VectorC Vec where   -- Instances of the "type class" must agree with function signatures.
    (·) (V3DCart x1 x2 x3) (V3DCart y1 y2 y3) = x1*y1+x2*y2+x3*y3
    (×) (V3DCart x1 x2 x3) (V3DCart y1 y2 y3) = (V3DCart (x2*y3-x3*y2) (x3*y1-x1*y3) (x1*y2-x2*y1))

SAVE STEP 2

Use your editor to save MyVetorsM.hs which is the final draft of the main function:

import MyVectorsF

main = do
    let a = make3DCV 2 4 5   -- Calls imported accessor function.
    let b = make3DCV 0 2 0

    print $ a · b
    print $ a × b

2. LOAD

Load has two steps. "Load Step 1" loads the vector functions. "Load Step 2" loads the main function.

LOAD STEP 1

As shown below, load the above MyVectorsF.hs file into GHCi:

Prelude>  :load MyVectorsF

[1 of 1] Compiling MyVectorsF      ( MyVectorsF.hs, interpreted )

Ok, modules loaded: MyVectorsF.

Prelude>  

LOAD STEP 2

As shown below, load the above MyVectorsM.hs file into GHCi:

Prelude>  :load MyVectorsM

[1 of 2] Compiling MyVectorsF       ( MyVectorsF.hs, interpreted )

[2 of 2] Compiling Main             ( MyVectorsM.hs, interpreted )

Ok, modules loaded: Main, MyVectorsF.

Prelude>  

Now that we have loaded Main, we can run functions in GHCi that were defined in Main.

3. RUN

As shown below, run the function main, in GHCi:

Prelude>  main

8.0
V3DCart (-10.0) 0.0 4.0

Prelude>  

If we want to see the type of the accessor function make3DCV we can do the following:

Prelude>  :load MyVectorsF

Ok, modules loaded: MyVectorsF.

Prelude>

Prelude>  :type make3DCV

make3DCV :: Float -> Float -> Float -> MyVectorsF.Vec

Prelude>

It says, if you want a vector, give me three Floats. However, if you want to see the type of MyVectorsF.Vec watch what happens. It says I am not going to tell you what a vector is.

Prelude>  :type MyVectorsF2.Vec
<interactive>:1:1: Not in scope: data constructor `MyVectorsF2.Vec'
Prelude> 

The representation of MyVectorsF.Vec is hidden from you, the user. 

4. COMPILE 

As shown below, compile MyVectorsM.hs in GHC:

Prelude>  :! ghc --make "*MyVectorsM"
[1 of 2] Compiling MyVectorsF       ( MyVectorsF.hs, MyVectorsF.o )
[2 of 2] Compiling Main                  ( MyVectorsM.hs, MyVectorsM.o )
Linking MyVectorsM.exe ...
Prelude>  

The compile is shown so you know it compiles without error.

C. COMMENTS

Use the program shown above as an example. Rewrite the example and make it your own program.

Repeat 1. thru 3. above until your new program works the way you want it to work. Each time you make changes in your editor to your program, make sure you save the file and load it in GHCi.

II. CONCLUSION

In this tutorial, you have been introduced to the advantages of using "Haskell Modules Data Hiding."

III. REFERENCE

Haskell Programming by Sankha Mukherjee

Haskell Tutorial 6 - Modules

HASKELL MODULES NO DATA HIDING

REVISED: Monday, February 12, 2024

Haskell Modules No Data Hiding.

I. HASKELL DATA MODULES

You are reading "Haskell Modules No Data Hiding",  the first half of the "Haskell Data Modules" tutorial.

"Haskell Modules Data Hiding"  is the second half.

The two parts of this tutorial are a very brief outline of "Haskell Programming Tutorial 6 - Modules" by Sankha Mukherjee.

A. SKELETON

We start off with the following file containing both the main function and the vector functions:

main = do

       print $ (2,4,5) · (0,1,0)

       print $ (2,4,5) × (0,1,0)

(·) :: (Float, Float, Float) -> (Float, Float, Float) -> Float
(·) (x1, x2, x3)(y1, y2, y3) =  x1*y1+x2*y2+x3*y3

(×) :: (Float, Float, Float) -> (Float, Float, Float) -> (Float, Float, Float)
(×) (x1, x2, x3)(y1, y2, y3) =  (x2*y3-x3*y2, x3*y1-x1*y3, x1*y2-x2*y1)

What happens if we need these vector functions in hundreds of other programs? One solution would be to copy past them into each of the other programs. 

However, what happens if we want to change a function; for example, changing from a three element tuple to a two element tuple? Changes might have to be made to hundreds of files that were copy pasted.

A good programming maintenance technique is to use modules.

One module for each group of related functions.

One module containing the main function.

B. FLESH ON BONES

1. SAVE

Save has two steps. "Save Step1" saves the module containing the vector functions. "Save Step 2" saves the main function.

SAVE STEP 1

Use your editor to save  MyVectorsF.hs the vector dot product, and vector cross product, function signatures and definitions. Notice both of these functions are tied to a particular data type; i.e., Float. Also notice each vector function assumes a "three element tuple". What do you do when you need the dot product or cross product of a vector which has less tuple elements or more tuple elements? That question will be answered in "Haskell Data Hiding".

module MyVectorsF where

(·) :: (Float, Float, Float) -> (Float, Float, Float) -> Float
(·) (x1, x2, x3)(y1, y2, y3) =  x1*y1+x2*y2+x3*y3

(×) :: (Float, Float, Float) -> (Float, Float, Float) -> (Float, Float, Float)
(×) (x1, x2, x3)(y1, y2, y3) =  (x2*y3-x3*y2, x3*y1-x1*y3, x1*y2-x2*y1)

SAVE STEP 2

Use your editor to save MyVetorsM.hs the main function. Notice by importing MyVectorsF you do not have to copy paste the vector functions into the main function.

import MyVectorsF

main = do

    print $ (2,4,5) · (0,1,0)

    print $ (2,4,5) × (0,1,0)

2. LOAD

Load has two steps. "Load Step 1" loads the vector functions. "Load Step 2" loads the main function.

LOAD STEP 1

As shown below, load the above MyVectorsF.hs file into GHCi:

Prelude>  :load MyVectorsF

[1 of 1] Compiling MyVectorsF      ( MyVectorsF.hs, interpreted )

Ok, modules loaded: MyVectorsF.

Prelude>  

LOAD STEP 2

As shown below, load the above MyVectorsM.hs file into GHCi:

Prelude>  :load MyVectorsM

[1 of 2] Compiling MyVectorsF       ( MyVectorsF.hs, interpreted )

[2 of 2] Compiling Main             ( MyVectorsM.hs, interpreted )

Ok, modules loaded: Main, MyVectorsF.

Prelude>  

Now that we have loaded Main, we can run functions in GHCi that were defined in Main.

3. RUN

As shown below, run the main function, in GHCi:

Prelude>  main

4.0
(-5.0,0.0,2.0)

Prelude>  

4. COMPILE 

As shown below, compile MyVectorsM.hs in GHC:

Prelude>  :! ghc --make "*MyVectorsM"
[1 of 2] Compiling MyVectorsF       ( MyVectorsF.hs, MyVectorsF.o )
[2 of 2] Compiling Main             ( MyVectorsM.hs, MyVectorsM.o )
Linking MyVectorsM.exe ...
Prelude>  

The compile is shown so you know it compiles without error.

C. COMMENTS

Use the program shown above as an example. Rewrite the example and make it your own program.

Repeat 1. thru 3. above until your new program works the way you want it to work. Each time you make changes in your editor to your program, make sure you save the file and load it in GHCi.

II. CONCLUSION

You have just received an introduced to "Haskell Modules No Data Hiding", the first half of the "Haskell Data Modules" tutorial.   "Haskell Modules Data Hiding" is the second half of "Haskell Data Modules".

III. REFERENCE

Haskell Programming by Sankha Mukherjee

Haskell Tutorial 6 - Modules