Introduction

Important notes on Haskel, category & related fields.

GitHub&GitLab parse ORG into HTML only partially. Good quality HTML export is in the `README.html`, it is hosted at https://blog.latukha.com/haskell-notes.html.

This is complex ORG notes file with LaTeX formulas. To get:

LaTeX formulas
Interlinks
Navigation

use capable editor.

If something - <<<This is a radio target>>> - for org-mode linking.

Elisp snippet for you to prettify ‘<<<Radio targets>>>’ to ’Radio targets’:

;;;; 2019-06-12: NOTE: Prettify '<<<Radio targets>>>' to be shown as 'Radio targets' when org-descriptive-links set
;;;; This is improvement of the code from: Tobias&glmorous: https://emacs.stackexchange.com/questions/19230/how-to-hide-targets
;;;; There exists library created from the sample: https://github.com/talwrii/org-hide-targets
(defcustom org-hidden-links-additional-re "\\(<<<\\)[[:print:]]+?\\(>>>\\)"
  "Regular expression that matches strings where the invisible-property of the sub-matches 1 and 2 is set to org-link."
  :type '(choice (const :tag "Off" nil) regexp)
  :group 'org-link)
(make-variable-buffer-local 'org-hidden-links-additional-re)

(defun org-activate-hidden-links-additional (limit)
  "Put invisible-property org-link on strings matching `org-hide-links-additional-re'."
  (if org-hidden-links-additional-re
      (re-search-forward org-hidden-links-additional-re limit t)
    (goto-char limit)
    nil))

(defun org-hidden-links-hook-function ()
  "Add rule for `org-activate-hidden-links-additional' to `org-font-lock-extra-keywords'.
    You can include this function in `org-font-lock-set-keywords-hook'."
  (add-to-list 'org-font-lock-extra-keywords
                '(org-activate-hidden-links-additional
                  (1 '(face org-target invisible org-link))
                  (2 '(face org-target invisible org-link)))))

(add-hook 'org-font-lock-set-keywords-hook #'org-hidden-links-hook-function)

SCHT: and metadata in :PROPERTIES: - of my org-drill practices, please just run org-drill-strip-all-data.

Definitions

<<<Abstraction>>>

SCHT: <2019-08-03 Sat>

abs away from, off (in absentia) tractus draw, haul, drag

Purified generalization of process.

Forgeting the details. Simplified approach.

* creates a new semantic level in which one can be absolutely precise.

It is great did to name an abstraction (Denotational semantics).

*

<<<Abstractions>>> <<<Abstracting>>> <<<Abstract>>>

<<<Algebra>>>

SCHT: <2019-09-16 Mon>

al-jabr - assemble parts. A system of algebra based on given axioms.

—

Abstract algebra - the study of number systems and operations within them.
Algebra - vector space over a field with a multiplication.

*

<<<Algebras>>>

<<<Algebraic>>>

Composite from simple parts. Also: Algebraic data type.

<<<Algebraic structure>>>

SCHT: <2019-07-22 Mon>

Algebraic structure on a set A (called carrier set or underlying set) is a collection of finitary operations on A. The set A with this structure is also called an algebra.

Algebraic structures include groups, rings, fields, and lattices. More complex structures can be defined by introducing multiple operations, different underlying sets, or by altering the defining axioms. Examples of more complex algebraic structures include vector spaces, modules, and algebras.

“Group-like structures”:

	Closure	Associativity	Identity	Invertability	Commutativity
Semigroupoid		\check
Small Category		\check	\check
Groupoid		\check	\check	\check
Magma	\check
Quasigroup	\check			\check
Loop	\check		\check	\check
Semigroup	\check	\check
Inverse Semigroup	\check	\check		\check
Monoid	\check	\check	\check
Group	\check	\check	\check	\check
Abelian group	\check	\check	\check	\check	\check
Ring	\check	\check	\check	\check	under +

*

<<<Algebraic structures>>>

<<<Alpha equivalence>>>

SCHT: <2019-07-23 Tue>

Alpha equivalence - if processes in expressions are literally the same, but names of parameters accordingly different (then they are synonyms).

<<<Ambigram>>>

SCHT: <2019-07-28 Sun>

ambi both γράμμα grámma written character

Object from different points of view has the same meaning.

While this word has two contradictory diametrically opposite meanings, one was chosen.

But it has… Both.

TODO: For merit of differentiating the meaning about different meaning referring to Tensor as object with many meanings.

Ancient Greek and Latin prefixes

SCHT: <2019-08-01 Thu>

Meaning	Greek prefix	Latin prefix
above, excess	hyper-	super-, ultra-
across, beyond, through	dia-	trans-
after		post-
again, back		re-
against	anti-	contra-, (in-, ob-)
all	pan	omni-
around	peri-	circum-
away or from	apo-, ap-	ab- (or de-)
bad, difficult, wrong	dys-	mal-
before	pro-	ante-, pre-
between, among		inter-
both	amphi-	ambi-
completely or very		de-, ob-
down		de-, ob-
four	tetra-	quad-
good	eu-	ben-, bene-
half, partially	hemi-	semi-
in, into	en-	il-, im-, in-, ir-
in front of	pro-	pro-
inside	endo-	intra-
large	macro-	(macro-, from Greek)
many	poly-	multi-
not*	a-, an-	de-, dis-, in-, ob-
on	epi-
one	mono-	uni-
out of	ek-	ex-, e-
outside	ecto-, exo-	extra-, extro-
over	epi-	ob- (sometimes)
self	auto-, aut-,auth-	ego-
small	micro-
three	tri-	tri-
through	dia-	trans-
to or toward	epi-	ad-, a-, ac-, as-
two	di-	bi-
under, insufficient	hypo-	sub-
with	sym-, syn-	co-. com-, con-
within, inside	endo-	intra-
without	a-, an-	dis- (sometimes)

*

<<<Greek prefix>>> <<<Latin prefix>>>

<<<Function application>>>

SCHT: <2019-09-16 Mon>

Bind argument to a parameter of a function and do a beta reduction.

*

<<<Apply>>> <<<Applying>>> <<<Application>>>

<<<Application memory>>>

Storage of	Block name
All not currently processing data	<<<Heap>>>
Function call, local variables	<<<Stack>>>
Static and global variables	Static/Global
Instructions	Binary code

When even Main invoked - it work in Stack, and called Stack frame. Stack frame size for function calculated when it is compiled. When stacked Stack frames exceed the Stack size - stack overflow happens.

<<<Argument>>>

arguere to make clear, to shine

* - evidence, proof, statement that results in system consequences.

<<<Argument of a function>>>

A value binded to the function parameter. Value/topic that the fuction would process/deal with.

Also see <<<Argument>>>.

*

<<<Function argument>>>

<<<As-pattern>>>

SCHT: <2019-08-01 Thu>

f list@(x, xs) = ...

<<<Binary>>>

SCHT: <2019-07-31 Wed>

Two of something.

<<<Binary tree>>>

data BinaryTree a
  = [[Leaf]]
  | [[Node]] (BinaryTree a) a (BinaryTree a)
  deriving (Eq, Ord, Show)

<<<Bind>>>

SCHT: <2019-07-23 Tue>

Establishing equality between two objects.

Most often:

equating variable to a value.
equating parameter of a function to an argument (variable/value/function). This term often is equated to applying argument to a function, which includes β-reduction.

*

<<<Binds>>> <<<Binding>>>

<<<Bottom value>>>

SCHT: <2019-07-24 Wed>

-- _ fits *.

Is a non-value placeholder for enything.

*

<<<Bottom>>> <<<Bottom values>>>

<<<Bound>>>

SCHT: <2019-07-24 Wed>

Haskell * type class means to have lowest value & highest value, so a bounded range of values.

*

<<<Bounded>>>

<<<Cartesian product>>>

$$ \mathcal{A} × \mathcal{B} ≡ ∑^∀{\overrightarrow{(a,b)}} \ | \ ∀ a ∈ \mathcal{A}, ∀ b ∈ \mathcal{B} $$.

Any function, functor is a subset of Cartesian product.

$$ ∑{(elem ∈ (\mathcal{A} × \mathcal{B}))} = cardinalityA × B $$

*

<<<Cardinalities>>>

<<<Case>>>

SCHT: <2019-08-01 Thu>

case x of
    | pattern1  -> ex1
    | pattern2  -> ex2
    | pattern3  -> ex3
    | otherwise -> exDefault

Syntatic sugar with guards allows usage of expressions:

case () of _
             | expr1     -> ex1
             | expr2     -> ex2
             | expr3     -> ex3
             | otherwise -> exDefault

<<<Category theory>>>

SCHT: <2019-08-04 Sun>

Category ($$ \mathcal{C} $$) consists of the basis:

Primitives:

Objects - $$ a^\mathcal{C} $$. A node. Object of some type. Often sets, than it is Set category.
Morphisms - $$ \overrightarrow{(a,b)}^\mathcal{C} $$ (AKA mappings).
Morphism composition - binary operation: $$ \overrightarrow{(a, b)}^\mathcal{C} ˆ \overrightarrow{(b, c)}^\mathcal{C} ≡ \overrightarrow{(a, c)}^\mathcal{C} \ | \ ∀ a, b, c ∈ \mathcal{C} $$. AKA principle of compositionality for morphisms.

Properties (or axioms):

Associativity of morphisms: $$ \overrightarrow{h} ˆ (\overrightarrow{g} ˆ \overrightarrow{f}) ≡ (\overrightarrow{h} ˆ \overrightarrow{g}) ˆ \overrightarrow{f} \ \ | \ \ \overrightarrow{f}_{a → b}, \overrightarrow{g}_{b → c}, \overrightarrow{h}_{c → d} $$.
Every object has exactly one (two-sided) identity morphism: $$ \overrightarrow{1}_x ˆ \overrightarrow{f}_{a → x} ≡ \overrightarrow{f}_{a → x}, \ \ \overrightarrow{g}_{x → b} ˆ \overrightarrow{1_x} ≡ \overrightarrow{g}_{x → b} \ \ | \ \ ∀ x \ ∃ \overrightarrow{1}_x, ∀ \overrightarrow{f}_{a → x}, ∀ \overrightarrow{g}_{x → b} $$.
Principle of compositionality.

From these axioms, can be proven that there is exactly one identity morphism for every object.

Object and morphism is complete abstractions for anything. In majority of cases under object is a state and morphism is a change.

*

<<<Category>>> <<<Categories>>>

<<<Abelian category>>>

SCHT: <2019-08-04 Thu>

Is which:

has a zero object,
has all binary biproducts,
has all kernel’s and cokernels,
(it has all pullbacks and pushouts)
all monomorphism’s and epimorphism’s are normal.

Abelian category is very stable; for example they are regular and they satisfy the snake lemma. The class of Abelian categories is closed under several categorical constructions.

There is notion of Abelian monoid (AKS Commutative monoid) and Abelian group (Commutative group).

<<<Composition>>>

Axiom of Category.

*

<<<Composable>>> <<<Compositions>>>

<<<Endofunctor category>>>

From the name, in this Category:

objects of $$ End $$ are Endofunctors $$ E^{\mathcal{C → C}} $$
morphisms are natural transformations between endofunctors

<<<Functor>>>

Functor is a map between categories. Translating objects and morphisms (as input can take morphism or object). They can preserve structure, or not.

Functor properties (axioms):

$$ F^{\mathcal{C → D}}(a) \quad | \quad ∀ a^\mathcal{D} $$ - every source object is mapped to object in target category
$$ \overrightarrow{(F^{\mathcal{C → D}}(a),F^{\mathcal{C → D}}(b))}^\mathcal{D} \ \ | \ \ ∀ \overrightarrow{(a, b)}^\mathcal{C} $$ - every source morphism is mapped to target category morphism between corresponding objects
$$ F^{\mathcal{C → D}}(\overrightarrow{g}^\mathcal{C} ˆ \overrightarrow{f}^\mathcal{C}) = F^{\mathcal{C → D}}(\overrightarrow{g}^\mathcal{C}) ˆ F^{\mathcal{C → D}}(\overrightarrow{f}^\mathcal{C}) \quad | \quad ∀ y=\overrightarrow{f}^\mathcal{C}(x), ∀ \overrightarrow{g}^\mathcal{C}(y) $$ - composition of morphisms translates directly

These axioms guarantee that composition of functors can be fused into one functor with composition of morphisms. This process called fusion.

In Haskell this axioms have form:

fmap id = id
fmap (f . g) = fmap f . fmap g

*

<<<Power set functor>>> <<<fmap>>> <<<Functors>>>

<<<Power set functor>>>

SCHT: <2019-08-17 Sat>

* - functor from set $$ S $$ to its power set $$ \mathcal{P}(S) $$.

Functor type class in Haskell corresponds to mathematical power set functor and allows to do function application inside type structure layers (denoted $$ f $$ or $$ m $$). IO is also such structure. Power set is unique to the set, power set functor is unique to the category (data type).

class Functor f where
  fmap :: (a -> b) -> f a -> f b

Functor instance must be of kind ( * -> * ), so instance for higher-kinded data type must be applied until this kind.

Composed functors lift functions through layers of structure.

Power set functor can be used to filter-out error cases (Nothing & Left cases) in Maybe, Either and related types.

<<<Power set functor laws>>>

SCHT: <2019-07-22 Mon>

Type instance of functor should abide this laws:

*

<<<Functor laws>>>

<<<Power set functor identity law>>>

fmap id == id

<<<Power set functor composition law>>>

fmap (f.g) == fmap f . fmap g

In words, it is if several functions are composed and then fmap is applied on them - it should be the same as if functions was fmapped and then composed.

<<<Lift>>>

SCHT: <2019-07-23 Tue>

fmap :: (a -> b) -> (f a -> f b)

Functor takes function a -> b and returns a function f a -> f b this is called lifting a function. Lift does a function application through the data structure.

*

<<<Lifting>>>

<<<Power set functor is a free monad>>>

SCHT: <2019-08-03 Sat>

Since:

$$ ∀ e ∈ S : ∃ \{e\} \, ∈ \, {\mathcal{P}(S)} \ \vDash \ ∀ e ∈ S : ∃ (e → \{e\}) ≡ unit $$
$$ ∀ \mathcal{P}(S) : \mathcal{P}(S) ∈ \mathcal{P}(S) \ \vDash \ ∀ \mathcal{P}(S) : ∃ (\mathcal{P}(\mathcal{P}(S)) → \mathcal{P}(S)) ≡ join $$

<<<Forgetful functor>>>

Functor that forgets part or all of what defines structure in domain category. $$ F^{\mathbf {Grp} → \mathbf {Set}} $$ that translates groups into their underlying sets. Constant functor is another example.

*

<<<Forgetful>>>

<<<Identity functor>>>

Maps all category to itself. All objects and morphisms to themselves.

Denotation: $$ 1^{\mathcal{C → C}} $$

<<<Endofunctor>>>

SCHT: <2019-07-28 Sun>

Is a functor which source (domain) and target (codomain) are the same category.

$$ F\mathcal{C → C}, E\mathcal{C → C} $$

*

<<<Endofunctors>>>

<<<Applicative functor>>>

* - Computer science term. Category theory name - lax monoidal functor. And in category $$ Set $$, and so in category $$ Hask $$ all applicatives and monads are strong (have tensorial strength).

* - sequences functorial computations (plain functors can’t).

(<*>) :: f (a -> b) -> f a -> f b

Requires Functor to exist. Requires Monoidal structure.

Has monoidal structure rules, separated from what happens inside structure.

Data type can have several applicative implementations.

Standard definition:

class Functor f => Applicative f where
  (<*>) :: f (a -> b) -> f a -> f b
  pure :: a -> f a

The old function:

ap :: Monad m => m (a -> b) -> m a -> m b

Control.Monad ap is old implementation of <*>.

*

<<<Applicative>>> <<<Applicatives>>> <<<Applicative functors>>>

<<<Applicative laws>>>

<<<Applicative identity law>>>

SCHT: <2019-08-02 Fri>

pure id <*> v = v

<<<Applicative composition law>>>

SCHT: <2019-07-27 Sat>

Function composition works regularly.

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

<<<Applicative homomorphism law>>>

SCHT: <2019-07-27 Sat>

Applying the function doesn’t change the structure around values.

pure f <*> pure x = pure (f x)

<<<Applicative interchange law>>>

SCHT: <2019-08-01 Thu>

On condition that internal order of evaluation is preserved - order of operands is not relevant.

u <*> pure y = pure ($ y) <*> u

<<<Applicative function>>>

<<<liftA*>>>

<<<liftA>>>

Essentially a fmap.

:type liftA
liftA :: Applicative f => (a -> b) -> f a -> f b

Lifts function into applicative function.

<<<liftA2>>> SCHT: <2019-07-23 Tue>

Lifts binary function across two Applicative functors.

liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c

liftA2 f x y == pure f <*> x <*> y

<<<liftA2 (<*>)>>>

liftA2 (<*>) is pretty useful. It can lift binary operation through the two layers: It is two-layer Applicative.

liftA2 :: Applicative f => (    a       ->  b  ->  c ) -> f      a        ->  f    b   ->  f    c
<*> :: Applicative f =>    (f  (a -> b) -> f a -> f b)
liftA2 (<*>) :: (Applicative f1, Applicative f2) =>      f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)

<<<liftA2 (liftA2 (<*>))>>>

liftA2 (<*>) 3-layer version.

<<<liftA3>>> SCHT: <2019-08-03 Sat>

liftA2 3-parameter version.

liftA3 f x y z == pure f <*> x <*> y <*> z

Conditional applicative computations

when :: Applicative f => Bool -> f () -> f ()

Only when True - perform an applicative computation.

unless :: Applicative f => Bool -> f () -> f ()

Only when False - perform an applicative computation.

<<<Special applicatives>>>

<<<Identity applicative>>>

-- Applicative f =>
-- f ~ Identity
type Id = Identity
instance Applicative Id
  where
    pure :: a -> Id a
    (<*>) :: Id (a -> b) -> Id a -> Id b

mkId = Identity
xs = [1, 2, 3]

const <$> mkId xs <*> mkId xs'
-- [1,2,3]

<<<Constant applicative>>>

It holds only to one value. The function does not exist and `b` is phantom.

-- Applicative f =>
-- f ~ Constant e
type C = Constant
instance Applicative C
  where
    pure :: a -> C e a
    (<*>) :: C e (a -> b) -> C e a -> C e b

pure 1
-- 1
pure 1 :: Constant String Int
-- Constant {getConstant = ""}

<<<Maybe applicative>>>

“There also can be no function at all.”

If function might not exist - embed `f` in Maybe structure, and use Maybe applicative.

-- f ~ Maybe
type M = Maybe
pure :: a -> M a
(<*>) :: M (a -> b) -> M a -> M b

<<<Either applicative>>>

`pure` is `Right`. Defaults to `Left`. And if there is two Left’s - to Left of the first argument.

<<<Validation applicative>>>

The Validation data type isomorphic to Either, but has accumulative Applicative on the error side. For this Applicative there is no corresponding Bind or Monad instance. Validation is an example of, “An applicative functor that is not a monad.” Because monad needs to process the result of computation - it needs to be able to process Left error statements, which is hard. Either monad on Left case just drops computation and returns this first Left.

<<<Monad>>>

SCHT: <2019-08-01 Thu>

μόνος monos sole μονάδα monáda unit

* - monoid in endofunctor category with $$ \overrightarrow{η} $$ (unit) and $$ \overrightarrow{μ} $$ (join) natural transformations.

If $$ \mathcal{C} $$ is a category, a monad on $$ \mathcal{C} $$ consists of:

an endofunctor $$ E^{\mathcal{C → C}} $$
two natural transformations:
- $$ \overrightarrow{η}^{1^{\mathcal{C}} → E} = {unit}^{Identity → E}(x) = f^{x → E(x)}(x) $$
- $$ \overrightarrow{μ}^{(E ˆ E) → E} = {join}^{(E ˆ E) → (Identity ˆ E)}(x) = | y = E(x) | = f^{E (y) → y}(y) $$

Where:

$$ 1^\mathcal{C} $$ denotes the $$ \mathcal{C} $$ identity functor,
$$ (E ˆ E) $$ - endofunctor $$ \mathcal{C → C} $$.

Definition with $$ \{E^{\mathcal{C → C}}, \, \overrightarrow{η}, \, \overrightarrow{μ}\} $$ (in Hask: ($$ \{e \, :: \, f \, a \, → \, f \, b, \ pure, \ join\} $$)) - is classic categorical, in Haskell minimal complete definition is $$ \{fmap, \, pure, \, (>>=)\} $$.

If there is a structure $$ S $$, and a way of taking object $$ x $$ into $$ S $$ and a way of collapsing $$ S ˆ S $$ - there probably a monad.

Mostly monads used for sequencing actions (computations) (that looks like imperative programming), with ability to dependend on previous chains. Note if monad is commutative - it does not order actions.

Monad can shorten/terminate sequence of computations. It is implemented inside Monad instance. For example Maybe monad on Nothing drops chain of computation and returns Nothing.

Monadic internals are Haskell data types, and as such - they can be consumed any number of times.

Same Monad and Applicative instances must be the same:

import Control.Monad (ap)
return == pure
ap == (<*>) -- + Monad requirement

Mathematics	Haskell	Math meaning
$$ E $$	= <$> ∷ Functor f ⇒ (a → b) → f a → f b =	power set functor (thou in CAT it can be any suiting endofunctor)
$$ \overrightarrow{η}_{ID → E} $$	= pure ∷ Applicative f ⇒ a → f a =	unit (natural transformation for functors $$ ID → P $$)
$$ \overrightarrow{μ}_{E ˆ E → E} $$	= join ∷ Monad f ⇒ f (f a) → f a =	join (natural transformation for functors $$ P ˆ P → P $$)

*

<<<Monads>>> <<<Monadic>>>

<<<Monad laws>>>

SCHT: <2019-07-27 Sat>

pure (return) should only put argument into structure.

<<<Monad left identity law>>> SCHT: <2019-07-23 Tue>

pure x >>= f == f x

Explanation:

>>= :: Monad f =>    f a  -> (a -> f b) -> f b
                  pure x >>=     f      == f x

Shows that >>= must get Argument internal to structure and apply it to the second argument.

<<<Monad right identity law>>> SCHT: <2019-08-06 Tue>

f >>= pure == f

Explanation:

>>= :: Monad f => f a  -> (a -> f b) -> f b
                  f   >>=    pure    == f

AKA it is a tacit description of a monad bind as endofunctor.

<<<Monad associativity law>>>

(m >>= f) >>= g == m >>= (\ x -> f x >>= g)

<<<Monad type class>>>

class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  (>>) :: m a -> m b -> m b
  return :: a -> m a

<<<MonadPlus type class>>> SCHT: <2019-08-02 Fri>

Is a monoid over monad, with additional rules. The precise set of rules (properties) not agreed upon. Class instances obey monoid & left zero rules, some additionally obey left catch and others left distribution.

Overall there * currently reforms (MonadPlus reform proposal) in several smaller nad strictly defined type classes.

Subclass of an Alternative.

* <<<Monadplus>>>

Functor -> Applicative -> Monad progression

<$> :: Functor     f =>   (a -> b)   -> f a -> f b
<*> :: Applicative f => f (a -> b)   -> f a -> f b
=<< :: Monad       f =>   (a -> f b) -> f a -> f b

pure & join are Natural transformations for the fmap.

<<<Monad function>>>

<<<Return function>>> SCHT: <2019-08-03 Sat>

return == pure

Nonstrict.

<<<Join function>>>

join :: Monad m => m (m a) -> m a

Flattens two layers of structure into one. Join is a generalization of `concat`.

The way to express ordering in lambda calculus is to nest.

* <<<join>>>join . fmap == (=<<)

-- b = f b
fmap        :: Monad f => (a -> f b) -> f a -> f (f b)
join        :: Monad f =>                      f (f a) -> f a
join . fmap :: Monad f => (a -> f b) -> f a            -> f b
flip    >>= :: Monad f => (a -> f b) -> f a            -> f b

<<<Bind function>>>

>>=         :: Monad f => f a -> (a -> f b) -> f b
join . fmap :: Monad f => (a -> f b) -> f a -> f b

Nonstrict.

The most ubiqutous way to >>= something is to use Lambda function:

getLine >>= \name -> putStrLn "age pls:"

Also very neet way is to bundle and handle Monad - is to bundle it with bind, and leave applied partially. And use that partial bundle as a function - every evaluation of the function would trigger evaluation of internal Monad structure. Thumbs up.

printOneOf ∷ Bool → IO ()
printOneOf False = putStr "1"
printOneOf  True = putStr "2"

quant ∷ (Bool → IO b) → IO b
quant = (>>=) (randomRIO (False, True))

recursePrintOneOf ∷ Monad m ⇒ (t → m a) → t → m b
recursePrintOneOf f x = (f x) >> (recursePrintOneOf f x)

main ∷ IO ()
main = recursePrintOneOf (quant) $ printOneOf

* <<<Monadic bind>>> <<<Monad bind>>> <<<Binder>>> <<<Binder function>>>(>>=)>>=(=<<)=<<<<<Sequencing operator>>> (>>) == (*>): SCHT: <2019-07-27 Sat>

Discards any resulting value of the action and sequence next action.

(>>) :: m a -> m b -> m b
(*>) :: f a -> f b -> f b

Applicative has a similar operator.

Monadic versions of list functions

sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)

Sequence gets the traversable of monadic computations and swaps it into monad computation of taverse. In the result the collection of monadic computations turns into one long monadic computation on traverse of data.

If some step of this long computation fails - monad fails.

mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)

mapM gets the AMB function, then takes traversable data. Then applies AMB function to traversable data, and returns converted monadic traversable data.

foldM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldl ::  Foldable t           => (b -> a ->   b) -> b -> t a ->   b

* is a monadic foldl.

b is initial comulative value, m b is a comulative bank. Right folding achieved by reversing the input list.

filterM :: Applicative m => (a -> m Bool) -> [a] -> m [a]
filter ::                   (a ->   Bool) -> [a] ->   [a]

Take Boolean monadic computation, filter the list by it.

zipWithM :: Applicative m => (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith  ::                  (a -> b ->   c) -> [a] -> [b] ->   [c]

Take monadic combine function and combine two lists with it.

msum :: (Foldable t, MonadPlus m) => t (m a) -> m a
sum  :: (Foldable t, Num a)       => t    a  ->   a

<<<liftM*>>><<<liftM>>>

Essentially a fmap.

liftM :: Monad m => (a -> b) -> m a -> m b

Lifts a function into monadic equivalent.

<<<liftM2>>>

Monadic liftA2.

liftM2 :: Monad m => (a -> b -> c) -> m a -> m a -> m c

Lifts binary function into monadic equivalent.

<<<Comonad>>>

SCHT: <2019-07-27 Sat>

Category $$ \mathcal{C} $$ comonad is a monad of opposite category $$ \mathcal{C}^op $$.

<<<Kleisli category>>>

SCHT: <2019-08-04 Sun>

Category $$ \mathcal{C} $$, $$ 〈E, \overrightarrow{η}, \overrightarrow{μ}〉 $$ monad over $$ \mathcal{C} $$.

Kleisli category $$ \mathcal{C}_T $$ of $$ \mathcal{C} $$:

$$ \mathrm{Obj}(\mathcal{C}T) \ = \ \mathrm{Obj}(\mathcal{C}) $$ $$ \mathrm{Hom}\mathcal{CT}(x,y) \ = \ \mathrm{Hom}\mathcal{C}(x,E(y)) $$

<<<Special monad>>>

<<<Identity monad>>>

Wraps data in the Identity constructor.

Useful: Creates monads from monad transformers.

Bind: Applies internal value to the bound function.

Code:

newtype Identity a = Identity { runIdentity :: a }

-- coerse is a function that directly moves data between type aliases
instance Functor Identity where
  fmap     = coerce

instance Applicative Identity where
  pure     = Identity
  (<*>)    = coerce

instance Monad Identity where
  m >>= k  = k (runIdentity m)

Example:

-- derive the State monad using the StateT monad transformer
type State s a = StateT s Identity a

<<<Maybe monad>>>

Something that may not be or not return a result. Any lookups into the real world, database querries.

Bind: Nothing input gives Nothing output, Just x input uses x as input to the bound function.

When some computation results in Nothing - drops the chain of computations and returns Nothing.

Zero: Nothing Plus: result in first occurence of Just else Nothing.

Code:

data Maybe a = Nothing | Just a

instance Monad Maybe where
  return         = Just
  fail           = Nothing
  Nothing  >>= _ = Nothing
  (Just x) >>= f = f x

instance MonadPlus Maybe where
  mzero             = Nothing
  Nothing `mplus` x = x
  x `mplus` _       = x

Example: Given 3 dictionaries:

Full names to email addresses,
Nicknames to email addresses,
Email addresses to email preferences.

Create a function that finds a person’s email preferences based on either a full name or a nickname.

data MailPref = HTML | Plain
data MailSystem = ...

getMailPrefs :: MailSystem -> String -> Maybe MailPref
getMailPrefs sys name =
  do let nameDB = fullNameDB sys
         nickDB = nickNameDB sys
         prefDB = prefsDB sys
  addr <- (lookup name nameDB) `mplus` (lookup name nickDB)
  lookup addr prefDB

<<<Either monad>>> SCHT: <2019-07-23 Tue>

When computation results in Left - drops other computations, returns the recieved Left.

<<<Error monad>>>

Someting that can fail, throw exceptions.

Failure records failure description. Binding uses successful values as input to the bound function, and passes failure information on without executing the bound function.

Useful: Composing functions that can fail. Handle exceptions, crate error handling structure.

Zero: empty error. Plus: if first argument failed then execute second argument.

<<<List monad>>>

Computations which may return 0 or more possible results.

Bind: The bound function is applied to all possible values in the input list and the resulting lists are concatenated into list of all possible results.

Useful: Building computations from sequences of non-deterministic operations.

Zero: [] Plus: (++)

* <<<[] monad>>><<<Reader monad>>>

Creates a read-only shared environment for computations.

The pure function ignores the environment, while >>= passes the inherited environment to both subcomputations.

type Reader r = ReaderT r Identity   -- equivalent to ((->) e), (e ->)

For (e ->):

Functor is (.)

fmap :: (b -> c) -> (a -> b) -> a -> c
fmap = (.)

Applicative:
- pure is const

pure :: a -> b -> a
pure x _ = x

(<*>) is:

(<*>) :: (a -> b -> c) -> (a -> b) -> a -> c
(<*>) f g = \a -> f a (g a)

Monad:

(>>=) :: (a -> b) -> (b -> a -> c) -> a -> c
(>>=) m k = Reader $ \r ->
                  runReader (k (runReader m r)) r

join :: (e -> e -> a) -> e -> a
join f x = f x x

runReader
  :: Reader r a  -- the Reader to run
  -> r  -- an initial environment
  -> a  -- extracted final value

Usage:

data Env = ...

createEnv :: IO Env
createEnv = ...

f :: Reader Env a
f = do
  a <- g
  pure a

g :: Reader Env a
g = do
  env <- ask  -- "Open the environment namespace into env"
  a <- h env  -- give env to h
  pure a

h :: Env -> a
...  -- use env and produce the result

main :: IO ()
main = do
  env <- createEnv
  a = runReader g env
  ...

In Haskell under normal circumstances impure functions should not directy call impure functions. h is an impure function, and createEnv is impure function, so they should have intermediary.

<<<Writer monad>>>

Computations which accumulate monoid data to a shared Haskell storage. So * is parametrized by monoidal type.

Accumulator is maintained separately from the returned values.

Shared value modified through Writer monad methods.

* frees creator and code from manually keeping the track of accumulation.

Bind: The bound function is applied to the input value, bound function allowed to <> to the accumulator.

type Writer r = WriterT r Identity

Example:

f :: Monoid b => a -> (a, b)
f a = if _condition_
         then runWriter $ g a
         else runWriter do
           a1 <- h a
           pure a1

g :: Monoid b => Writer b a
g a = do
  tell _value1_  -- accumulator <> _value1_
  pure a  -- observe that accumulator stored inside monad and only a main value needs to be returned

h :: Monoid b => Writer b a
h a = do
  tell _value2_  -- accumulator <> _value_
  pure a

runWriter :: Writer w a -> (a, w)  -- Unwrap a writer computation as a (result, accumulator) pair.
                                   -- The inverse of writer.

WriterT, Writer unnecessarily keeps the entire logs in the memory. Use fast-logger for logging.

<<<State monad>>>

Computations that pass-over a state.

The bound function is applied to the input value to produce a state transition function which is applied to the input state.

Pure functional language cannot update values in place because it violates referential transparency.

type State s = StateT s Identity

Binding copies and transforms the state parameter through the sequence of the bound functions so that the same state storage is never used twice. Overall this gives the illusion of in-place update to the programmer and in the code, while in fact the autogenerated transition functions handle the state changes.

Example type: State st a

State describes functions that consume a state and produce a tuple of result and an updated state.

Monad manages the state with the next process:

Where:

f - processsor making function
pA, pAB, pB - state processors
sN - states
vN - values

Bind with a processor making function from state procesor (pA) creates a new state processor (pAB). The wrapping and unwrapping by State/runState is implicit.

<<<Alternative type class>>>

SCHT: <2019-07-27 Sat>

Monoid over applicative. Has left catch property.

Allows to run simolteniously several instances of a computation (or computations) and from them yeld one result by law from (<|>) :: Type -> Type -> Type.

Minimal complete definition:

empty :: f a    -- The identity element of <|>
(<|>) :: f a -> f a -> f a    -- Associative binary operation

*

<<<Alternative>>>

<<<Monoidal functor>>>

Functors between monoidal categories that preserves monoidal structure.

<<<Fusion>>>

fmap f . fmap g = fmap (f . g)

This functor axiom allows to greatly simplify computations, it is called *.

<<<Hask category>>>

Category of Haskell where objects are types and morphisms are functions.

It is a hypothetical category at the moment, since undefined and bottom values break the theory, is not Cartesian closed, it does not have sums, products, or initial object, () is not a terminal object, monad identities fail for almost all instances of the Monad class.

That is why Haskell developers think in subset of Haskell where types do not have bottom values. This only includes functions that terminate, and typically only finite values. The corresponding category has the expected initial and terminal objects, sums and products, and instances of Functor and Monad really are endofunctors and monads.

Hask contains subcategories, like Lst containing only list types.

Haskell and Category concepts:

Things that take a type and return another type are type constructors.
Things that take a function and return another function are higher-order functions.

*

<<<Hask>>>

<<<Magma>>>

Set with a binary operation which form a closure.

<<<Mag category>>>

The category of magmas, denoted $$ Mag $$, has as objects - sets with a binary operation, and morphisms given by homomorphisms of operations (in the universal algebra sense).

*

<<<MAG>>> <<<Magma category>>> <<<Category of magmas>>>

<<<Semigroup>>>

SCHT: <2019-07-28 Sun>

Magma with associative property.

Defined in Haskell as:

class Semigroup a where
(<>) :: a -> a -> a

*

<<<Semigroups>>>

<<<Monoid>>>

SCHT: <2019-07-24 Wed>

Semigroup with Identity element.

Ideally fits as an accumulation class.

class Monoid m where
mempty :: m
mappend :: m -> m -> m
mappend = (<>)
mconcat :: [m] -> m
mconcat = foldr mappend mempty

* can be simplified to category with a single object, remember that monoid operation is a composition of morphisms operation in category. For example to represent the whole non-negative integers with the one object and morphism “$$ 1 $$” is absolutely enough, composition operation is “$$ + $$”.

import Data.Monoid
do
  show (mempty :: Num a => Sum a)
  -- "Sum {getSum = 0}"
  show $ Sum 1
  -- "Sum {getSum = 1}"
  show $ (Sum 1) <> (Sum 1) <> (Sum 1)
  -- "Sum {getSum = 3}"
  -- ...

Also backwards - any single-object category is a monoid. Category has an identity requirement and associativity of composition requirement, which makes it a free monoid.

*

<<<Monoidal>>> <<<Monoids>>>

<<<Monoid laws>>>

<<<Monoid left identity law>>> SCHT: <2019-07-28 Sun>

mempty <> x = x

<<<Monoid right identity law>>>

x <> mempty = x

<<<Monoid associativity law>>>

x <> mempty = x (y <> z) = (x <> y) <> z
mconcat = foldr (mempty <>)

Everything associative can be mappend.

<<<Commutative monoid>>>

SCHT: <2019-08-03 Sat>

Commutative law: $$ x ˆ y = y ˆ x $$ Very helpful at concurrent or distributed processing.

Enables a lot of abilities and concurrency in monoidal structures.

* <<<Abelian monoid>>>

<<<Group>>>

Monoid with inverse for every element (element operation with inverse gives identity)

* <<<Groups>>><<<Commutative group>>> Group operation obeys the axiom of commutativity.* <<<Abelian group>>><<<Ring>>> SCHT: <2019-07-24 Wed>

Commutative group under + & monoid under ×, + × connected by distributive property.

and × are generalized binary operations of addition and multiplication. × has no requirement for commutativity.

Example: set of same size square matricies of numbers with matrix operations form a ring.

* <<<Rings>>>

<<<Morphism>>>

SCHT: <2019-07-23 Tue>

μορφή morphe form Map between two objects in a category.

General description: Arrow from one to enother that denotes something.

On a level of objects: morphism is some maybe structure-preserving map from one mathematical structure to another one of the same type.

Morphism is a generalization ($$ f(x*y) ≡ f(x) \diamond f(y) $$) of homomorphism ($$ f(x*y) ≡ f(x) * f(y) $$). Under morphism almost always is meaning of homomorphism-like properties.

If morphism corresponds to function requirements - than it is a function. Morphism can be anything.

*

<<<Morphisms>>> <<<Arrow>>> <<<Arrows>>>

<<<Homomorphism>>>

SCHT: <2019-07-22 Mon>

ὁμός homos same (was chosen becouse of initial Anglish mistranslation to “similar”) μορφή morphe form similar form

Homomorphism - operation-preserving map between two algebraic structures of the same type (groups, rings, vector spaces…).

$$ f^{A → B}_homomorphism = f(x * y) = f(x) \diamond f(y) | (A_set, *_operation), (B_set, \diamond_operation) $$.

The concept of homomorphism has been generalized under the name of morphism to many other structures that either do not have an underlying set, or are not algebraic.

Homomorphisms send identity morphisms to identity morphisms and inverses to inverses.

* homomorphism - map between * and preserves * operations case * of:

semigroup
monoid
groups
ring
linear map
module
algebra

*

<<<Homomorphic>>>

<<<Identity morphism>>>

Identity morphism - or simply identity: $$ x ∈ C : \; id_x=1_x : x → x $$ Composed with other morphism gives same morphism.

Corresponds to Reflexivity and Automorphism.

<<<Identity>>>

SCHT: <2019-07-22 Mon>

Identity only possible with morphism. See Identity morphism.

There is also distinct Zero value.

<<<Two-sided identity of a predicate>>>

SCHT: <2019-07-23 Tue>

$$ P(e,a)=P(a,e)=a \ | \ ∃ e ∈ S, ∀ a ∈ S $$ $$ P() $$ is commutative.

Predicate

<<<Left identity of a predicate>>>

$$ ∃ e ∈ S, ∀ a ∈ S : \; P(e,a)=a $$

Predicate

<<<Right identity of a predicate>>>

SCHT: <2019-08-05 Mon>

$$ P(a,e)=a \; | \; ∃ e ∈ S, ∀ a ∈ S $$

Predicate

<<<Identity function>>>

Return itself. (\ x.x)

id :: a -> a

<<<Monomorphism>>>

μονο mono only μορφή morphe form

Initial set of f is fully uniquely mapped onto the image of f. Left is mono (uniquely) mapped to the right, so left domain can be equal or less to the right codomain. It is injective. It always has a inverse morphism.

$$ f^{X → Y}, ∀ x ∈ X \, ∃ y=f(x) \vDash f(x) = f_mono(x) $$ - from homomorphism context $$ f_mono ˆ g1 ≡ f_mono ˆ g2 \vDash \; g1 ≡ g2 $$ - from general morphism context Thus it is left canselable.

*

<<<Monomorphic>>>

<<<Epimorphism>>>

SCHT: <2019-07-22 Mon>

επι epi on, over μορφή morphe form

Image fully uses codomain - epimorphism. It is surjective.

$$ f^{X → Y}, ∀ y ∈ Y \, ∃ f(x) \vDash f(x)=f_epi(x) $$ - from homomorphism context $$ g_1 ˆ f_epi ≡ g_2 ˆ f_epi \vDash \; g_1 = g_2 $$ - from general morphism context Thus epimorphism is right canselable.

Left is epi to the right. So left is bigger or equal then the right. And right is a projection of the left.

*

<<<Epimorphic>>>

<<<Isomorphism>>>

ἴσος isos equal μορφή morphe form

Not equal, but equal for current intents and purposes. Morphism that has inverse. Almost equal, but not quite: (Integer, Bool) & (Bool, Integer) - but can be transformed losslessly into one another.

Bijective homomorphism is also isomorphism.

$$ f-1, b → a ˆ fa → b ≡ id^a, \; fa → b ˆ f-1, b → a ≡ id^b $$

2 reasons for non-isomorphism:

function at least ones collapses a values of domain into one value in codomain
image (of a function in codomain) does not fill-in codomain. Then isomorphism can exists for image but not whole codomain.

Categories are isomorphic if there $$ R ∘ L = ID

*

<<<Isomorphic>>>

<<<Endomorphism>>>

SCHT: <2019-08-01 Thu>

ενδο endo internal μορφή morphe form

Morphism whose domain equals the codomain. Epimorphism is a Monoid, because of category composition.

<<<Automorphism>>>

SCHT: <2019-07-27 Sat>

α\upsilonτ\omicron auto self μορφή form form

Endomorphism that is Isomorphism.

Corresponds to Identity and Reflexivity.

*

<<<Automorphic>>>

*

<<<Endomorphic>>>

<<<Catamorphism>>>

κατά kata downward μορφή morphe form

Denotes the unique homomorphism from an initial algebra into some other algebra.

In functional programming, catamorphisms provide generalizations of folds of lists to arbitrary algebraic data types, which can be described as initial algebras. The dual concept is that of anamorphism that generalize unfolds. A hylomorphism is the composition of an anamorphism followed by a catamorphism.

*

<<<Catamorphic>>>

<<<Kernel>>>

SCHT: <2019-07-24 Wed>

Kernel of a homomorphism is a number that measures the degree homomorphism fails to meet injectivity (AKA be monomorphic). It is a number of domain elements that fail injectivity:

elements not included into morphism
elements that collapse into one element in codomain

thou Kernel $$ [ x | x ← 0 || x ≥ 2 ] $$.

Denotation: $$ \operatorname{ker}T = \{ \mathbf{v} ∈ V:T(\mathbf{v}) = \mathbf{0}_W \} $$.

<<<Kernel homomorphism>>>

SCHT: <2019-07-23 Tue>

Morphism of elements from the kernel. Map of elements that make main morphism not monomorphic (injective).

<<<Anamorphism>>>

Morphism from a coalgebra to the final coalgebra for that endofunctor. Is a function that generates a sequence by repeated application of the function to its previous result.

<<<Object>>>

Mathematical structure. Morphisms preserve structure.

*

<<<Structure>>> <<<Structures>>> <<<Objects>>>

<<<Terminal object>>>

Terminal object - is an object i: $$ ∃ ! (x → i) \ | \ ∃ i ∈ \mathcal{C} , \; ∀ x ∈ \mathcal{C} $$.

<<<Initial object>>>

SCHT: <2019-08-01 Thu>

Initial object - is an object i: $$ ∃ ! (i → x) \ | \ ∃ i ∈ \mathcal{C}, \ ∀ x ∈ \mathcal{C} $$.

<<<Set category>>>

SCHT: <2019-07-24 Wed>

Category in which objects are sets.

<<<Natural transformation>>>

* ($$ \overrightarrow{η}^\mathcal{D} $$) is transforming : $$ \overrightarrow{η}^\mathcal{D} ˆ F^{\mathcal{C → D}} = G^{\mathcal{C → D}} $$. Right there was seen that * allows higher-language of Category theory, talking about the composition and transformation of complex theory entities.

Roughly * is:

trans :: F a -> G a

It is a process of transforming $$ F^{\mathcal{C → D}} $$ into $$ G^{\mathcal{C → D}} $$ using existing morphisms in target category $$ \mathcal{D} $$.

Since it uses morphisms - it is structure-preserving transformation of one functor into another. And since it uses only existing morphisms - it exists only when transformation is possible with existing morphisms.

Existence of * between two functors means they are somehow related.

Can be observed to be a “morphism of functors”, especially in functor category. * by $$ \overrightarrow{η}^\mathcal{D}_{y^{\mathcal{C}}}(\overrightarrow{(x,y)}^\mathcal{C}) ˆ F^{\mathcal{C → D}}(\overrightarrow{(x,y)}^\mathcal{C}) = G^{\mathcal{C → D}}(\overrightarrow{(x,y)}^\mathcal{C}) ˆ \overrightarrow{η}^\mathcal{D}_{x^{\mathcal{C}}}(\overrightarrow{(x,y)}^\mathcal{C}) $$, often written short $$ \overrightarrow{η}_b ˆ F(\overrightarrow{f}) = G({\overrightarrow{f}) ˆ \overrightarrow{η}_a $$. Notice that the $$ \overrightarrow{η}^\mathcal{D}_{x^{\mathcal{C}}}(\overrightarrow{(x,y)}^\mathcal{C}) $$ depends on objects&morphisms of $$ \mathcal{C} $$.

In words, * depends on $$ F $$ and $$ G $$ functors, ability of $$ D $$ morphisms to do a homotopy of $$ F $$ to $$ G $$, and *:

for every object in $$ \mathcal{C} $$ picks natural transformation component in $$ \mathcal{D} $$.
for every morphism in $$ \mathcal{C} $$ picks the commuting diagram in $$ \mathcal{D} $$, called <<<naturality square>>>.

Also see: Natural transformation in Haskell

*

<<<Natural transformations>>>

<<<Natural transformation component>>>

$$ \overrightarrow{η}\mathcal{D}(x) = F\mathcal{D}(x) → G\mathcal{D}(x) \ | \ x ∈ \mathcal{C} $$

*

<<<Component of natural transformation>>>

<<<Natural transformation in Haskell>>>

* is a family of morphisms parametrized by type (parametric polymorphism functions) between endofunctors (Functor, Applicative, Monad).

* in Hask is $$ F \ a → G \ a $$ - repackages data into another container, never modifies the object content, it only if - can delete it. If other - that can not be called a *.

<<<Hom set>>>

Collection of all morphisms $$ hom^\mathcal{C}(a,b) \ | \ ∀ ( a → b ) ∈ \mathcal{C} $$.

<<<Category dual>>>

Category duality behaves like a logical inverse.

Inverse $$ \mathcal{C} $$ = $$ \mathcal{C}^op $$ - invert the direction of morphisms.

(Morphisms include all their compositions)

Any statement in the terms of $$ \mathcal{C} $$ the logical inverse is true in $$ \mathcal {C}^op $$.

Properties:

Opposite preserves products: $$ (\mathcal{C} × \mathcal{D})^op ≅ \mathcal{C}^op × \mathcal{D}^op $$
Opposite preserves functors: $$ (F^\mathcal{C → \mathcal{D}})^op ≅ F^\mathcal{C^op → \mathcal{D}^op} $$
Opposite preserves slices: $$ (\mathcal{F} ↓ \mathcal{G})^op ≅ (\mathcal{G}^op ↓ \mathcal{F}^op) $$

*

<<<Opposite category>>> <<<Opposite categories>>> <<<Category duality>>> <<<Duality>>> <<<Dual category>>>

<<<Closure>>>

SCHT: <2019-07-27 Sat>

$$ f(x) = f^{\mathcal{X → X}} \ | \ ∀ x ∈ \mathcal{X} $$, $$ \mathcal{X} $$ is closed under $$ f $$, it is a trivial case when operation is legitimate for all values of the domain.

Operation on members of the domain always produces a members of the domain. The domain is closed under the operation.

In the case when there is a domain values for which operation is not legitimate/not exists:

$$ f(x) = f^{\mathcal{V → X}} \ | \ \mathcal{V ∈ X}, ∀ x ∈ \mathcal{V} $$, $$ \mathcal{X} $$ is closed under $$ f $$.

*

<<<Closed>>>

<<<Coalgebra>>>

Structures that are dual (in the category-theoretic sense of reversing arrows) to unital associative algebras. Every coalgebra, by vector space duality, reversing arrows - gives rise to an algebra. In finite dimensions, this duality goes in both directions. In infinite - it should be determined.

<<<Concatenate>>>

Link together sequences.

<<<Conjunction>>>

SCHT: <2019-07-26 Fri>

Logical AND

Multiplies cardinalities.

Haskell kind:

* *

<<<Constructor>>>

SCHT: <2019-08-03 Sat>

Type constructor
Data constructor

Also see: Constant

<<<Context>>>

SCHT: <2019-07-23 Tue>

Constraint placed on the types under polymorphic variables. Written before the main type signature and denoted:

TypeClass a =>

*

<<<Contexts>>>

<<<Contravariant>>>

The property of basis, in which if new basis is a linear combination of the prior basis, and the change of basis inverse-proportional for the description of a Tensors in this basisis.

Denotation: Components for contravariant basis denoted in the upper indices: $$ Vⁱ = x $$

The inverse of a covariant transformation is a contravariant transformation. Whenever a vector should be invariant under a change of basis, that is to say it should represent the same geometrical or physical object having the same magnitude and direction as before, its components must transform according to the contravariant rule.

*

<<<Contravariant cofunctor>>> <<<Contravariant functor>>> - More inline term is Contravariant cofunctor

<<<Covariant>>>

The property of basis, in which if new basis is a linear combination of the prior basis, and the change of basis proportional for a descriptions of Tensors in this basisis.

Denotation: Components for covariant basis denoted in the upper indices: $$ V_i = x $$

*

<<<Covariant functor>>> <<<Covariant cofunctor>>>

<<<Data type>>>

SCHT: <2019-07-22 Mon>

Set of values. For type to have sence the values share some sence, properties.

*

<<<Type>>> <<<Types>>> <<<Data types>>>

<<<Actual type>>>

SCHT: <2019-07-22 Mon>

Data type recieved by ->inferring->compiling->execution.

<<<Algebraic data type>>>

Composite type formed by combining other types.

*

<<<AlgDT>>>

<<<Cardinality>>>

SCHT: <2019-07-27 Sat>

Number of possible implementations for a given type signature.

Disjunction, sum - adds cardinalities. Conjunction, product - multiplies cardinalities.

<<<Data constant>>>

* - constant value; nullary data constructor.

<<<Data constructor>>>

One instance that inhabit data type.

<<<data declaration>>>

Data type declaration is the most general and versatile form to create a new data type. Form:

data [context =>] type typeVars1..n
  = con1  c1t1..i
  | ...
  | conm  cmt1..q
  [deriving]

<<<Dependent type>>>

When type and values have relation between them. Type has restrictions for values, value of a type variable has a result on the type.

*

<<<Dependent types>>>

<<<Gen type>>>

SCHT: <2019-08-08 Thu>

Generator. Gen type is to generate pseudo-random values for parent type. Produces a list of values that gets infinitely cycled.

<<<Higher-kinded data type>>>

SCHT: <2019-07-23 Tue>

Any combination of * and ->

Type that take more types as arguments.

*

<<<Higher-kinded data types>>>

<<<newtype declaration>>>

SCHT: <2019-08-04 Sun>

Creates a new type from old type using a new constructor.

newtype FirstName = FirstName String

Data will have exactly the same representation at runtime, as the type that is wrapped.

newtype Book = Book (Int, Int)

      (,)
      / \
Integer Integer

<<<Principal type>>>

SCHT: <2019-08-14 Wed>

The most generic data type that still typechecks.

<<<Product data type>>>

SCHT: <2019-07-22 Mon>

Algebraic data type formed by logical conjunction (AND ’ ‘).

<<<Proxy type>>>

Proxy type holds no data, but has a phantom parameter of arbitrary type (or even kind). Able to provide type information, even though has no value of that type (or it can be may too costly to create one).

data Proxy a = ProxyValue

let proxy1 = (ProxyValue :: Proxy Int) -- a has kind `Type`
let proxy2 = (ProxyValue :: Proxy List) -- a has kind `Type -> Type`

<<<Static typing>>>

Static typechecking occurs at compile level.

<<<Structural type>>>

Mathematical type. They form into structural type system.

*

<<<Structural>>>

<<<Structural type system>>>

Strict global hierarchy and relationships of types and their properties. Haskell type system is *. In most languages typing is name-based, not structural.

*

<<<Structural typing>>>

<<<Sum data type>>>

Algebraic data type formed by logical disjunction (OR ‘|’).

<<<Tuple>>>

Data type that stores multiple values withing a single value. Tuples by arity:

empty, unit - 0
pair, <<<two-tuples>>> - 2
<<<thriple>>>, three-tuple - 3

<<<Type alias>>>

SCHT: <2019-09-11 Wed>

Create new type constructor, and use all data structure of the base type.

<<<Type class>>>

SCHT: <2019-07-30 Tue>

Type system construct that adds a support of ad hoc polymorphism.

Type classes make a nice way for defining behaviour over many objects at once.

*

<<<Type classes>>> <<<Typeclass>>> <<<Typeclasses>>>

<<<Arbitrary type class>>>

SCHT: <2019-07-28 Sun>

Type class of QuickCheck.Arbitrary (that is reexported by QuickCheck) for creating a generator/distribution of values. Useful function is arbitrary - that autogenerates values.

<<<Arbitrary function>>>

Depends on type and generates values of that type.

<<<CoArbitrary type class>>>

Pseudogenerates a function basing on resulting type.

coarbitrary :: CoArbitrary a => a -> Gen b -> Gen b

*

<<<CoArbitrary>>>

<<<Type class inheritance>>>

Type class has a superclass.

<<<Derived instance>>>

SCHT: <2019-08-10 Sat>

Type class instances sometimes can be automatically derived from the parent types.

Type classes such as Eq, Enum, Ord, Show can have instances generated based on definition of data type.

*

<<<Derived>>> <<<Deriving>>>

<<<Type constant>>>

SCHT: <2019-07-27 Sat>

* - Nullary type constructor.

<<<Type constructor>>>

Name of data type.

<<<type declaration>>>

SCHT: <2019-08-03 Sat>

Synonim for existing type. Uses the same data constructor.

type FirstName = String

Used to distinct one entities from other entities, while they have the same type. Also main type functions can operate on a new type.

<<<Typed hole>>>

SCHT: <2019-07-22 Mon>

In GHC if to use placeholder _ or _name, GHC on evaluation of the hole would supply derived type information and information to help fill the gap.

*

<<<Typed holes>>>

<<<Type inference>>>

Automatic data type detection of expression.

*

<<<Inferring>>> <<<Infer>>> <<<Infers>>> <<<Inferred>>>

<<<Type class instance>>>

SCHT: <2019-07-22 Mon>

Unique type class->type pairing implementation of functions.

<<<Type rank>>>

Weak ordering of types.

The rank of polymorphic type shows at what level of nesting forall quantifier appears. Count-in only quantifiers that appear to the left of arrows.

f1 :: forall a b. a -> b -> a    ==    fi :: a -> b -> c
g1 :: forall a b. (Ord a, Eq b) => a -> b -> a    ==    g1 :: (Ord a, Eq b) => a -> b -> a

f1, g1 - rank-1 types. Haskell itself implicitly adds universal quantification.

f2 :: (forall a. a->a) -> Int -> Int
g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int

f2, g2 - rank-2 types. Quantificator is on the left side of a →. Quantificator shows that type on the left can be overloaded.

f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool

f3 - rannk3-type. Has rank-2 types on the left of a →.

f :: Int -> (forall a. a -> a)
g :: Int -> Ord a => a -> a

f, g are rank 1. Quantifier appears to the right of an arrow, not to the left. These types are not Haskell-98. They are supported in RankNTypes.

Type inference in Rank-2 is possible, but not higher.

*

<<<Type ranks>>> <<<Rank type>>> <<<Rank types>> <<<Rank-1 type>>> <<<Rank-1 types>>> <<<Rank-2 type>>> <<<Rank-2 types>>> <<<Rank-3 type>>> <<<Rank-3 types>>>

<<<Type variable>>>

Refer to an unspecified type in Haskell type signature.

<<<Unlifted type>>>

SCHT: <2019-08-09 Fri>

Type that directly exist on the hardware. The type abstraction can be completely removed. With unlifted types Haskel type system directly manages data in the hardware.

*

<<<Unlifted types>>>

<<<Data structure>>>

<<<Cons cell>>>

Cell that values may inhabit.

<<<Construct>>>

(:) :: a -> [a] -> [a]

*

<<<Cons>>>

<<<Leaf>>>

_

<<<Node>>>

SCHT: <2019-07-23 Tue>

 *
/ \

<<<Linear type>>>

SCHT: <2019-07-23 Tue>

Type system and algebra that also track the multiplicity of data. There are 3 general linear type groups:

0 - exists only at type level and is not allowed to be used at value level. Aka `s` in ST-Trick.
1 - data that is not duplicated
1< - all other data, that can be duplicated multiple times.

*

<<<Linear types>>>

<<<NonEmpty list data type>>>

Data.List.NonEmpty Has a Semigroup instance but can’t have a Monoid instance. It never can be an empty list.

data NonEmpty a = a :| [a]
  deriving (Eq, Ord, Show)

:| - an infix data costructor that takes two (type) arguments. In other words :| returns a product type of left and right

<<<Session type>>>

* - allows to check that behaviour conforms to the protocol.

So far very complex not very productive (& well-established) topic.

<<<Declaration>>>

SCHT: <2019-07-25 Thu>

Binding the name to expression.

<<<Differential operator>>>

SCHT: <2019-07-23 Tue>

Denotation. $$ \frac{d}{dx}, \, D, \, D_x, \, ∂_x. $$ Last one is partial.

$$ e^t{\frac{d{dx}}} $$ - Shift operator.

*

<<<Differential>>>

<<<Disjunction>>>

SCHT: <2019-07-24 Wed>

OR

<<<Dispatch>>>

Send, transmission, reference.

<<<Distributive axiom>>>

Set S and two binary operators + ×:

$$ x × (y + z) = (x × y) + (x × z) $$ - × is left-distributive over +
$$ (y + z) × x = (y × x) + (z × x) $$ - × is right-distributive over +
left-&right-distributive - × is distributive over +

*

<<<Distributive rule>>> <<<Distributive property>>> <<<Distributive law>>> <<<Distributive>>>

<<<Dynamic scope>>>

The name resolution depends upon the program state when the name is encountered, which is determined by the execution context or calling context.

<<<Effect>>>

Observable action.

<<<Evaluation>>>

SCHT: <2019-07-24 Wed>

For FP see Bind.

<<<Expected type>>>

SCHT: <2019-08-03 Sat>

Data type inferred from the text of the code.

<<<Expression>>>

Finite combination of a symbols that is well-formed according to rules that depend on the context.

*

<<<Expressions>>>

<<<Closed-form expression>>>

SCHT: <2019-08-01 Thu>

Closed-form expression - a mathematical expression that can be evaluated in a finite number of operations. It may contain constants, variables, certain “well-known” operations (e.g., + − × ÷), and functions (e.g., nth root, exponent, logarithm, trigonometric functions, and inverse hyperbolic functions), but usually no limit.

<<<RHS>>>

Right-hand side of the expression.

<<<LHS>>>

Left-hand side of the expression.

<<<Redex>>>

SCHT: <2019-07-30 Tue>

Reducible expression.

<<<First-class>>>

Can be used as value.
Passed as an argument.

From 1&2 -> can include itself.

<<<First-order logic>>>

SCHT: <2019-08-07 Wed>

Formal notation systems of sciences that use quantifier, variables over non-logical objects, allows the use of expressions that contain variables. Distinguishes from propositional logic, which does not use quantifiers, relations.

*

<<<Predicate logic>>> <<<First-order predicate calculus>>>

<<<Free variable>>>

SCHT: <2019-07-30 Tue>

Variable in the fuction that is not bound by the head. Until there are * - function stays partially applied.

<<<Function>>>

A varying quantity depends on another quantity.

$$ x ∈ X, y ∈ Y : \; fX → Y = \overset{\rightharpoonup}{G}(x,y) $$

Directionality and property of invariability emerge from one another.

-- domain func codomain
   *      ->   *

$$ y(x) = (zx² + bx + 3 \ | \ b = 5) $$ ^ ^ ^^ ^ ^

| \_Parameter \__Name__of__the__function

		\_Var \__Constants
	\__Bound__variable
\_Free variable

Lambda abstraction is a function. Function is a mathematical operation.

Function = Total function = Pure function. Function theoretically posible to momoized. Partial function. Inverse function - often partially exists (partial function).

*

<<<Functions>>> <<<Bound variable>>>

<<<Arity>>>

SCHT: <2019-07-22 Mon>

Number of parameters of the function.

nullary - f()
unary - f(x)
binary - f(x,y)
ternary - f(x,y,z)
n-ary - f(x,y,z..)

<<<Bijection>>>

Function complete one-to-one pairing of elements of domain and codomain (image). It means function both surjective (so image == codomain) and injective (every domain element has unique correspondence to the image element).

For bijection inverse always exists.

Bijective operation holds the equivalence of domain and codomain.

Denotation:

⤖
>->>
f : X ⤖ Y

LaTeX needed to combine symbols: $$ \newcommand*{\twoheadrghtarrowtail}{\mathrel{\rightarrowtail\kern-1.9ex\twoheadrightarrow}} f : X \twoheadrghtarrowtail Y $$

*

<<<Bijective>>> <<<Bijective function>>>

<<<Combinator>>>

Function without free variables. Higher-order function that uses only function application and other combinators.

\a -> a
\ a b -> a b
\f g x -> f (g x)
\f g x y -> f (g x y)

Not combinators:

\ xs -> sum xs

Informal broad meaning: referring to the style of organizing libraries centered around the idea of combining things.

<<<Function application>>>

SCHT: <2019-07-23 Tue>

Function application is applying the function parameter to an argument from its domain to obtain the resulting value from its range.

*

<<<Applied>>> <<<Apply>>>

<<<Function body>>>

Expression that haracterizes the process.

<<<Function composition>>>

(.) :: (b -> c) -> (a -> b) -> a -> c

a -> (a -> b) -> (b -> c) -> c

In Haskell inline composition requires:

h.g.f $ i

*

<<<Composition>>> <<<Compose>>> <<<Composed>>>

<<<Function head>>>

Is a part with Name of the function and it’s paramenter. AKA: f(x)

<<<Function range>>>

The range of a function refers to either the codomain or the image of the function, depending upon usage. Modern usage almost always uses range to mean image. So, see Function image.

<<<Higher-order function>>>

Function arity > 1.

----

Has function as a parameter. Evaluates to function.

*

<<<HOF>>>

<<<Fold>>>

SCHT: <2019-08-03 Sat>

Higher-order function returns accumulated result from recursive data structure applying a function.

<<<Injection>>>

Function one-to-one injects from domain into codomain.

Keeps distinct pairing of elements of domain and image. Every element in image coresponds to one element in domain.

$$ ∀ a,b ∈ X, \; f(a)=f(b) ⇒ a=b $$

$$ ∃ (inverse \ function) \ | \ ∀ (injective \ function) $$

Denotion:

↣
>->
f : X ↣ Y

$f : X \rightarrowtail Y$

Corresponds to Monomorphism.

*

<<<Injective>>> <<<Injective function>>> <<<Injectivity>>>

<<<Partial function>>>

SCHT: <2019-07-22 Mon>

One that does not cover all domain. Unsafe and causes trouble.

<<<Purity>>>

SCHT: <2019-08-03 Sat>

Referentially transparent function.

*

<<<Pure>>> <<<Pure function>>>

<<<Sectioning>>>

SCHT: <2019-07-27 Sat>

Writing function in a parentheses. Allows to pass around partially applied functions.

<<<Surjection>>>

SCHT: <2019-07-23 Tue>

Function uses codomain fully.

$$ ∀ y ∈ Y, ∃ x ∈ X $$

Denotation:

↠
->>
f : X ↠ Y

$$ f : X \twoheadrightarrow Y $$

Corresponds to Epimorphism.

*

<<<Surjective>>> <<<Surjective function>>>

<<<Unsafe function>>>

SCHT: <2019-08-20 Tue>

Function that does not cover at least one edge case.

*

<<<Unsafe>>>

<<<Variadic>>>

SCHT: <2019-08-02 Fri>

Variadic function has a indefinite arity. Assepts a variable number of arguments.

<<<Domain>>>

Source set of a function in $$ X → Y $$.

<<<Codomain>>>

SCHT: <2019-07-28 Sun>

Codomain - target set of a function in $X → Y$.

<<<Open formula>>>

SCHT: <2019-08-01 Thu>

Function with arity.

<<<Recursion>>>

Repeated function application allow computing results that may require indefinite amount of work.

*

<<<Recursive>>>

<<<Base case>>>

SCHT: <2019-07-29 Mon>

A part of a recursive function that trivially produces result.

<<<Tail recursion>>>

Tail calls are recursive invocantions of itself.

<<<Fundamental theorem of algebra>>>

SCHT: <2019-07-23 Tue>

Any non-constant single-variable polynomial with complex coefficients has at least one complex root. Also derives that the field of complex numbers is algebraically closed.

<<<Guerrilla patch>>>

SCHT: <2019-08-03 Sat>

* changing code/applying patch sneakily - and possibility incompatibility with other at runtime. Monkey patch is derivative term.

<<<Homotopy>>>

ὁμός homós same

One can be “continuously deformed” into the other.

For example - functions, functors. Natural transformation is a homotopy of functors.

*

<<<Homotopies>>> <<<Homotopic>>>

<<<Idiom>>>

SCHT: <2019-07-23 Tue>

* - something having a meaning that can not be derived from the conjoined meanings. Meaning can be special for language speakers or human with particular knowledge.

* can also mean Applicative functor.

*

<<<Idiomatic>>>

<<<Iff>>>

SCHT: <2019-08-03 Sat>

If and only if, exectly when, just. Denotation: $$ \iff $$

<<<Impredicative>>>

SCHT: <2019-07-22 Mon>

Self-referencing definition.

—

Antonym - Predicative.

<<<Infix>>>

SCHT: <2019-08-01 Thu>

Form of wrinting of operaton application in-between variables.

<<<Inhabit>>>

What values inhabit data type

<<<Interface>>>

Point of mutual meeting. Code behind interface determines how data is consumed.

<<<IO>>>

SCHT: <2019-07-22 Mon>

Type for values whose evaluations has a posibility to cause side effects or return unpredictable result. Haskell standard uses monad for constructing and transforming IO actions. IO actions can be evaluated multiple times.

IO data type has unpure imperative actions inside. Haskell is pure Lambda calculus, and unpure IO integrates in the Haskell purely (type system abstracts IO unpurity inside IO data type).

IO collects effects sequences one after another:

:{
twoBinds :: IO ()
twoBinds =
  putStrLn "First:" >>
  getLine >>=
  \a ->
  putStrLn "Second:" >>
  getLine >>=
  \b ->
  putStrLn ("\nFirst: "
    ++ a ++ ".\nSecond "
    ++ b ++ ".")
main = twoBinds
:}

<<<Kind>>>

Kind -> Type -> Data

<<<Lambda calculus>>>

Universal model of computation. Which means * can implement any Turing machine. Based on function abstraction and application by substituting variables and binding values.

* has lambda terms:

variable ($$ x $$)
application ($$ (ts) $$)
abstraction (lambda function) ($$ (λ x . t) $$)

*

<<<Lambda term>>> <<<Lambda terms>>>

<<<Lambda abstraction>>>

Lambda term that has a head and body and is applied to an argument. $$ λ x.x+1 $$

\ x -> x + 1
^^

<<<Lambda cube>>>

λ-cube shows the dimentions of generalization from simply typed Lambda calculus to Calculus of constructions.

Each dimension of the cube corresponds to a new way of making objects depend on other objects:

(First-class polymorphism) - terms allowed to depend on types, corresponding to polymorphism.
(Higher-rank polymorphism) - types depending on terms, corresponding to dependent types.
(Type class) - types depending on types, corresponding to type operators.

*

<<<λ-cube>>> <<<λ-cube>>>

<<<Lambda function>>>

Function of Lambda calculus. $$ λ x y.x^2 + y^3 $$ ^^ ^ ^

| \__parameter \___parameter

	\___BODY
		\__variable
	\__variable
	(_____)

(___) \____HEAD

<<<Lambda expression>>>

See Lambda function

<<<Anonymous function>>>

Lambda function without the name to bind to.

<<<β-reduction>>>

SCHT: <2019-07-23 Tue>

Equation of a parameter to its bound variable, and reducing parameter from the head.

*

<<<β reduction>>> <<<Beta-reduction>>> <<<Beta reduction>>>

<<<β-normal form>>>

SCHT: <2019-08-18 Sun>

No beta reduction is possible.

*

<<<β normal from>>> <<<Beta normal form>>> <<<Beta-normal form>>>

<<<Calculus of constructions>>>

Extends the Curry–Howard correspondence to the proofs in the full intuitionistic predicate calculus (includes proofs of quantified statements). Type theory, typed programming language, and constructivism (phylosophy) foundation for mathematics. Directly relates to Coq programming language.

*

<<<<<<CoC>>>>>>

<<<Curry–Howard correspondence>>>

Computer programs are mathematical proofs.

*

<<<Curry–Howard isomorphism>>>

<<<Currying>>>

Translating the evaluation of a multiple argument function (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument.

*

<<<Curry>>>

<<<Hindley–Milner type system>>>

SCHT: <2019-08-05 Mon>

Classical type system for the Lambda calculus with Parametric polymorphism and Type inference. Where types marked as polymorphic variables, and overall type inference is possible all over the code. Also known as Damas–Milner or Damas–Hindley–Milner system.

<<<Reduction>>>

See Beta reduction

*

<<<Reducible>>>

<<<β-η normal form>>>

No β-reduction and no η-reduction are possible in expression.

*

<<<beta-eta normal form>>> <<<beta eta normal form>>>

<<<η-abstraction>>>

SCHT: <2019-08-02 Fri>

$$ (λ x.Mx) \xleftarrow[η]{} M $$

\ x -> g . f $ x
\ x -> g . f     --eta-abstraction

*

<<<η-reduction>>> <<<η-conversion>>> <<<η abstraction>>> <<<η reduction>>> <<<η conversion>>> <<<eta-abstraction>>> <<<eta-reduction>>> <<<eta-conversion>>> <<<eta abstraction>>> <<<eta reduction>>> <<<eta conversion>>>

<<<Lense>>>

Library to provide Haskell (functional language without mutation) the get-ters and set-ters of imperative language.

<<<Level of code>>>

SCHT: <2019-07-23 Tue>

There are mainly three levels of Haskell code.

*

<<<Code level>>>

<<<Term level>>>

SCHT: <2019-07-24 Wed>

Level of code that works with data types.

<<<Type level>>>

Level of code that does logical execution.

<<<Compile level>>>

SCHT: <2019-07-23 Tue>

Level of code when code compiles/compiled.

*

<<<Compilation level>>>

<<<Runtime level>>>

Level of code when binary code executes in machine.

<<<Lexical scope>>>

SCHT: <2019-07-28 Sun>

Scope bound by the structure of source code where the named entity is defined.

*

<<<Static scope>>>

<<<Local scope>>>

SCHT: <2019-07-30 Tue>

Scope applies only in (current) area.

*

<<<Local>>>

<<<Module>>>

Importable organization unit.

<<<Modulus>>>

Special numbers where arithmetic wraps around in modular arithmetic.

*

<<<Moduli>>> - plural.

<<<Monkey patch>>>

SCHT: <2019-07-31 Wed>

From Guerrilla patch.

* is a way for program to modify supporting system software affecting only the running instance of the program.

<<<Nothing>>>

Any Haskell expression can’t return nothing.

<<<Operation>>>

SCHT: <2019-07-30 Tue>

Function. Word used in mathematics. Often a symbol, infix, binary.

<<<Binary operation>>>

$$ ∀ (a,b) ∈ S, ∃ P(a,b)=f(a,b): S × S → S $$

*

<<<Binary operations>>>

<<<Operator>>>

SCHT: <2019-08-03 Sat>

Function that denoted by symbol.

<<<Shift operator>>>

Shift operator defined by Lagrange through Differential operator. $$ T^t \, = \, e^t{\frac{d{dx}}} $$

*

Shift

<<<Orphan type instance>>>

SCHT: <2019-07-23 Tue>

Type instance that appeared from inconsistent code base. Duplicate of instance, or instance present on type class or on the type level.

Solution for addressing orphan instances:

You defined the type but not the type class?

Put the instance in the same module as the type so that the type cannot be imported without its instances.

You defined the type class but not the type?

Put the instance in the same module as the type class definition so that the type class cannot be imported without its instances.

Neither the type nor the type class are yours?

Define your own newtype wrapping the original type and now you’ve got a type that “belongs” to you for which you can rightly define type class instances. There are means of making this less annoying which we’ll discuss later.

<<<Parameter>>>

SCHT: <2019-07-22 Mon>

παρά para subsidiary μέτρον metron measure

Or Formal Parameter. Named varible of a function.

Argument is a supplied value to a function.

*

<<<Parameters>>>

<<<Partial application>>>

Part of function parameters applied.

*

<<<Partially applied>>>

<<<Pattern guard>>>

SCHT: <2019-08-01 Thu>

Allows check a list of pattern matches against functions, and then proceed.

(pattern1) <- (funcCheck1)

, (pattern2) <- (funcCheck2) = RHS

lookup :: Eq a => a -> [(a, b)] -> Maybe b

addLookup l a1 a2
   | Just b1 <- lookup a1 l
   , Just b2 <- lookup a2 l
   = val1 + val2
{-...other equations...-}

Run functions, they must succeed. Then pattern match results to val1, val2. Only if successful - execute the equation.

Default in Haskell 2010.

*

<<<Pattern guards>>>

<<<Permutation>>>

SCHT: <2019-07-27 Sat>

Bijective function from domain to itself.

<<<Phrase>>>

* - composable expression.

<<<Point-free>>>

SCHT: <2019-08-09 Fri>

Paradigm where function only describes the morphism itself.

Process of converting function to point-free. If brackets () can be changed to $ then $ equal to composition:

\ x -> g (f x)
\ x -> g $ f x
\ x -> g . f $ x
\ x -> g . f     --eta-abstraction

\ x1 x2 -> g (f x1 x2)
\ x1 x2 -> g $ f x1 x2
\ x1 x2 -> g . f x1 $ x2
\ x1    -> g . f x1

*

<<<Pointfree>>> <<<Tacit>>> <<<Tacit programming>>>

<<<Blackbird>>>

SCHT: <2019-09-11 Wed>

(.).(.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c

Composition of compositions (.).(.). Allows to compose-in a binary function f1(c) (.).(.) f2(a,b).

\f g x y -> f (g x y)

*

<<<.) .>>> <<<(.).(.)>>> <<<Composition of compositions>>>

<<<Swing>>>

SCHT: <2019-07-27 Sat>

swing :: (((a -> b) -> b) -> c -> d) -> c -> a -> d
swing = flip . (. flip id)
swing f = flip (f . runCont . return)
swing f c a = f ($ a) c

<<<Squish>>>

f >>= a . b . c =<< g

<<<Polymorphism>>>

SCHT: <2019-07-23 Tue>

πολύς polús many

At once several forms.

Abstract over data types.

Antonym - Monomorphism.

Types:

*

<<<Polymorphic>>>

<<<Levity polymorphism>>>

Levity polymprphism is when polymorphism works with lifted and unlifted types.

<<<Parametric polymorphism>>>

Abstracting over data types by parameter.

In most languages named as ‘Generics’ (generic programming).

Types:

<<<Rank-1 polymorphism>>>

SCHT: <2019-07-27 Sat>

Parametric polymorphism in rank-1 types by type variables.

*

<<<Prenex>>> <<<Prenex polymorpism>>>

<<<Let-bound polymorphism>>>

It is property chosen for Haskell type system. Haskell is based on Hindley-Milner type system, it is let-bound. It means that to have strict type inference - if `let` and `where` declarations a polymorphic - $λ$ declarations - should be not. So:

foo :: (Int, Char)
foo = (\f -> (f 1, f 'a')) id

Is illegal in Haskell.

Lambda-bound function (i.e., one passed as argument to another function) cannot be instantiated in two different ways, if there is a let-bound polymorphism.

<<<Constrained polymorphism>>>

Constrained Parametric polymorphism.

<<<Ad hoc polymorphism>>>

SCHT: <2019-07-22 Mon>

Artificial constrained polymorphism dependent on incoming data type. Achieved by creating a type class functions. It is interface dispatch mechanism by data types.

Commonly known as overloading.

* <<<Constraint>>> <<<Constraints>>>

<<<Impredicative polymorphism>>>

SCHT: <2019-07-22 Mon>

The most powerful form of Parametric polymorphism. First see Impredicative.

Impredicative polymorphism allows type τ entities with polymorphic types that can contain type τ itself. $$ T = ∀ X. X → X : \; T ∈ X \vDash T ∈ T $$ This approach has Russell’s paradox (and its form - Girard’s paradox).

*

<<<First-class polymorphism>>>

<<<Higher-rank polymorphism>>>

Means that polymorphic types can apper within other types (types of function). There is a cases where higher-rank polymorphism than the a Ad hoc - is needed. For example where ad hoc polymorphism is used in constraints of several different implementations of functions, and you want to build a function on top - and use the abstract interface over these functions.

-- ad-hoc polymorphism
f1 :: forall a. MyType Class a => a -> String    ==    f1 :: MyType Class a => a  -> String
f1 = -- ...

-- higher-rank polymorphism
f2 :: Int -> (forall a. MyType Class a => a -> String) -> Int
f2 = -- ...

By moving `forall` inside the function - we can achive higher-rank polymorphism.

From: https://news.ycombinator.com/item?id=8130861

Higher-rank polymorphism is formalized using System F, and there are a few implementations of (incomplete, but decidable) type inference for it - see e.g. Daan Leijen's research page [1] about it, or my experimental implementation [2] of one of his papers. Higher-rank types also have some limited support in OCaml and Haskell.

Useful example aslo a ST-Trick monad.

*

<<<Rank-n polymorphism>>>

<<<Subtype polymorphism>>>

Allows to declare usage of a Type and all of its Subtypes. T - Type S - Subtype of Type <: - subtype of $$ S <: T = S ≤ T $$

Subtyping is: If it can be done to T, and there is subtype S - then it also can be done to S. $$ S <:T : \; f^{T → X} ⇒ f^{S → X} $$

<<<Row polymorphism>>>

Is a lot like Subtype polymorphism, but alings itself on allowence (with | r) of subtypes and types with requested properties.

printX :: { x :: Int | r } -> String
printX rec = show rec.x

printY :: { y :: Int | r } -> String
printY rec = show rec.y

-- type is inferred as `{x :: Int, y :: Int | r } -> String`
printBoth rec = printX rec ++ printY rec

<<<Kind polymorphism>>>

Achieved using a phantom type argument in the data type declaration.

;;         * -> *
data Proxy a = ProxyValue

Then, by default the data type can be inhabited and fully work being partially defined. But multiple instances of kind polymorphic type can be distinguished by their particular type.

Example is the Proxy type:

data Proxy a = ProxyValue

let proxy1 = (ProxyValue :: Proxy Int) -- * :: Proxy Int
let proxy2 = (ProxyValue :: Proxy a)   -- * -> * :: Proxy a

<<<Linearity polymorphism>>>

Leverages linear types. For exampe - if fold over a dynamic array:

In basic Haskell - array would be copied at every step.
Use low-level unsafe functions.
With Linear type function we guarantee that the array would be used only at one place at a time.

So, if we use a function (* -o * -o -o *) in foldr - the fold will use the initial value only once.

<<<Pragma>>>

SCHT: <2019-07-23 Tue>

Pragma - instruction to the compiler that specifies how a compiler should process the code. Pragma in Haskell have form:

{-# PRAGMA options #-}

<<<LANGUAGE pragma>>>

SCHT: <2019-07-23 Tue>

Controls what variations of the language are permitted. It has a set of allowed options: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html, which can be supplied.

<<<LANGUAGE option>>>

Useful by default

import EmptyCase
import FlexibleContexts
import FlexibleInstances
import InstanceSigs
import MultiParamTypeClasses

<<<AllowAmbiguousTypes>>>

Allow type signatures which appear that they would result in an unusable binding. However GHC will still check and complain about a functions that can never be called.

<<<ApplicativeDo>>>

Enables an alternative in-depth reduction that translates the do-notation to the operators <$>, <*>, join as far as possible.

For GHC to pickup the patterns, the final statement must match one of these patterns exactly:

pure E
pure $ E
return E
return $ E

When the statements of do expression have dependencies between them, and ApplicativeDo cannot infer an Applicative type - GHC uses a heuristic $$ O(n^2) $$ algorithm to try to use <*> as much as possible. This algorithm usually finds the best solution, but in rare complex cases it might miss an opportunity. There is aslo $$ O(n^3) $$ algorithm that finds the optimal solution: -foptimal-applicative-do.

Requires ap = <*>, return = pure, which is true for the most monadic types.

Allows use of do-notation with types that are an instance of Applicative and Functor
In some monads, using the applicative operators is more efficient than monadic bind. For example, it may enable more parallelism.

The only way it shows up at the source level is that you can have a do expression with only Applicative or Functor constaint.

It is possible to see the actual translation by using -ddump-ds.

<<<ConstrainedClassMethods>>>

Enable the definition of further constraints on individual class methods.

<<<CPP>>>

Enable C preprocessor.

<<<DeriveFunctor>>>

SCHT: <2019-08-05 Mon>

Automatic deriving of instances for the Functor type class. For type power set functor is unique, its derivation inplementation can be autochecked.

<<<ExplicitForAll>>>

SCHT: <2019-07-23 Tue>

Allow explicit forall quantificator in places where it is implicit by Haskell.

<<<FlexibleContexts>>>

Ability to use complex constraints in class declaration contexts. The only restriction on the context in a class declaration is that the class hierarchy must be acyclic.

class C a where
  op :: D b => a -> b -> b

class C a => D a where ...

$$ C :> D $$, so in C we can talk about D.

Synergizes with ConstraintKinds.

<<<FlexibleInstances>>>

SCHT: <2019-08-04 Sun>

Allow type class instances types contain nested types.

instance C (Maybe Int) where ...

Implies TypeSynonymInstances.

<<<GeneralizedNewtypeDeriving>>>

SCHT: <2019-07-23 Tue>

Enable GHC’s newtype cunning generalised deriving mechanism.

newtype Dollars = Dollars Int
  deriving (Eq, Ord, Show, Read, Enum, Num, Real, Bounded, Integral)

(In old Haskell-98 only Eq, Ord, Enum could been inherited.)

<<<ImplicitParams>>>

SCHT: <2019-07-29 Mon>

Allow definition of functions expecting implicit parameters. In the Haskell that has static scoping of variables allows the dynamic scoping, such as in classic Lisp or ELisp. Sure thing this one can be puzzling as hell inside Haskell.

<<<LambdaCase>>>

SCHT: <2019-08-19 Mon>

Enables expressions of the form:

\case { p1 -> e1; ...; pN -> eN }

-- OR

\case
  p1 -> e1
  ...
  pN -> eN

<<<MultiParamTypeClasses>>>

Implies: ConstrainedClassMethods Enable the definitions of typeclasses with more than one parameter.

class Collection c a where

<<<MultiWayIf>>>

SCHT: <2019-07-23 Tue>

Enable multi-way-if syntax.

if | guard1 -> expr1
   | ...
   | guardN -> exprN

<<<OverloadedStrings>>>

SCHT: <2019-07-23 Tue>

Enable overloaded string literals (string literals become desugared via the IsString class). Now string literal has type:

(IsString a) => a

The usual string syntax can be used, e.g., for ByteString, Text, and other variations of string like types. Now they can be used in pattern matches as char->integer translations. To pattern match Eq must be derived.

To use class IsString - import it from GHC.Ext

<<<PartialTypeSignatures>>>

Partial type signature containins wildcards, placeholders (_, _name). Allows programmer to which parts of a type to annotate and which to infer. Also applies to constraint part.

As untuped expression, partly typed can not polymorphicly recurse.

-Wno-partial-type-signatures supresses infer warnings.

<<<RankNTypes>>>

SCHT: <2019-07-23 Tue>

Enable types of arbitrary rank. See Type rank.

Implies ExplicitForAll.

Allows forall quantifier:

Left side of →
Right side of →
as argument of a constructor
as type of a field
as type of an implicit parameter
used in pattern type signature of Lexically scoped type variables

It can synergyze with ScopedTypeVariables.

<<<ScopedTypeVariables>>>

By default type variables do not have a scope except inside type signatures where they are used.

When there are internall type signatures provided in the code block (where, let, etc.) they (main type description of a function and internal type descriptions) restrain one-another and become not trully polymorphic, which creates a bounding interdependency of types that GHC would complain about.

* option provides the lexical scope inside the code block for type variables that have forall quantifier. Because they are now lexiacally scoped - those type variables are used across internal type signatures.

For details see: https://ocharles.org.uk/guest-posts/2014-12-20-scoped-type-variables.html

Implies ExplicitForAll.

<<<TupleSections>>>

SCHT: <2019-07-23 Tue>

Allow tuple section syntax:

(, True)
(, "I", , , "Love", , 1337)

<<<TypeApplications>>>

Allow type application syntax:

read @Int 5

:type pure @[]
pure @[] :: a -> [a]

:type (<*>) @[]
(<*>) @[] :: [a -> b] -> [a] -> [b]

--

instance (CoArbitrary a, Arbitrary b) => Arbitrary (a -> b)

λ> ($ 0) <$> generate (arbitrary @(Int -> Int))

<<<TypeSynonymInstances>>>

SCHT: <2019-07-27 Sat>

Now type synonim can have it’s own type class instances.

<<<UndecidableInstances>>>

Permit instances which may lead to type-checker non-termination.

GHC has Instance termination rules regardless of FlexibleInstances FlexibleContexts.

<<<ViewPatterns>>>

SCHT: <2019-08-02 Fri>

size (view -> Unit) = 1
size (view -> Arrow t1 t2) = size t1 + size t2

(expression → pattern): take what is came to match - apply the expression, then do pattern-match, and return what originally came to match.

Semantics:

variables of expression and pattern are shared

if expression :: t1 -> t2 && pattern :: t2, then (expression → pattern): t1.

* are like pattern guards that can be nested inside of other patterns. * are a convenient way to pattern-match algebraic data type.

<<<DatatypeContexts>>>

SCHT: <2019-07-23 Tue>

Allow contexts in data types.

data Eq a => Set a = NilSet | ConsSet a (Set a)

-- NilSet :: Set a
-- ConsSet :: Eq a => a -> Set a -> Set a

Considered misfeature, deprecated, going to be removed.

How to make a GHC LANGUAGE extension

In `libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs` add new constructor to the `Extension` type

data Extension
  = Cpp
  | OverlappingInstances
  ...
  | Foo

`/main/DynFlags.hs` extend `xFlagsDeps`:

xFlagsDeps = [
  flagSpec "AllowAmbiguousTypes" LangExt.AllowAmbiguousTypes,
  ...
  flagSpec "Foo"                 LangExt.Foo
]

It is for basic case. For testing, parser see further: https://blog.shaynefletcher.org/2019/02/adding-ghc-language-extension.html

<<<Predicative>>>

SCHT: <2019-07-22 Mon>

Non-self-referencing definition.

—

Antonym - Impredicative.

<<<Principle of compositionality>>>

SCHT: <2019-07-28 Sun>

The meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them.

<<<Ψ-combinator>>>

SCHT: <2019-08-16 Fri>

Transforms two of the same type into one of some type. By applying mediate transformation, and applying combination of them into result.

import Data.Function (on)
on :: (b -> b -> c) -> (a -> b) -> a -> a -> c

*

<<<Psi-combinator>>> <<<On-combinator>>>

<<<Quantifier>>>

SCHT: <2019-08-01 Thu>

Specifies the quantity of specimens.

Two most common quantifiers $$ ∀ $$ (Forall) and $$ ∃ $$ (Exists). $$ ∃ ! $$ - one and only one (exists only unique).

*

<<<Quantification>>> <<<Quantifiers>>> <<<Quantified>>>

<<<Forall quantifier>>>

Permits to not infer the type, but to use any that fits. The variant depends on the LANGUAGE option used: ScopedTypeVariables RankNTypes ExistentialQuantification

*

<<<Forall>>>

<<<Referential transparency>>>

SCHT: <2019-07-22 Mon>

Returns the same output given the same values to evaluate. So: * expression can be replaced with its corresponding resulting value without change for program’s behavior. * functions are pure.

*

<<<Referentially transparent>>>

<<<Relation>>>

SCHT: <2019-08-13 Tue>

Relationship between two objects. Is not directed and not limited.

*

<<<Relations>>> <<<Relationship>>>

<<<REPL>>>

Interactive CLI. Read-eval-print loop.

<<<Scope>>>

SCHT: <2019-07-24 Wed>

Area where binds are accessible.

<<<Semantics>>>

Philosophical study of meaning.

<<<Operational semantics>>>

Properties, such as correctness, safety or security, are verified by constructing proofs from logical assertion s about execution and procedures.

Good to solve in-point localized tasks. Process of abstraction.

<<<Denotational semantics>>>

SCHT: <2019-08-03 Sat>

Construction of mathematical objects (called denotations), that describe the meanings. In Haskell often abstractions that are ment (denotations), implemented directly in the code, sometimes exist over the code - allowing to reason and implement.

* are composable.

Good to achive more broad approach/meaning.

Also see Abstraction.

<<<Axiomatic semantics>>>

Describing effect of operation on assertions about the overall state.

Good for examining interconnections. Empirical process.

<<<Set>>>

SCHT: <2019-09-11 Wed>

Well-defined collection of distinct objects.

*

<<<Sets>>>

<<<Closed set>>>

Closed set - a set whose complement is an open set. Closed set is a form of Closed-form expression. Set can be closed in under a set of operations.

<<<Power set>>>

For some $$ \mathit{set} \mathcal{S} $$, the power set ($$ \mathcal{P(S)} $$) is a set of all subsets of $$ \mathcal{S} $$, including $$ \{\} $$ & $$ \mathcal{S} $$ itself. Denotation: $$ \mathcal{P(S)} $$

<<<Hom-set>>>

SCHT: <2019-07-27 Sat>

Collection of all morphisms (and compositions of morphisms) from object to object. Collection of morphisms is not nesessary a set, but in practice - is.

Denotation: $$ hom(X,Y) $$

$$ hom_C(x,y) = (∀ f^{x → y}) = hom(x,y) = C(x,y) $$ Denotation was not standartized.

<<<Hom-functor>>>

SCHT: <2019-07-27 Sat>

$$ hom:\mathcal{C}^op × \mathcal{C} → Set $$, for locally small category $$ \mathcal{C} $$. Functor from the product of $$ \mathcal{C} $$ with opposite category to the category of sets.

Denotation variants: $$ H_A = \mathrm{Hom}(-, A) $$ $$ h_A = {\cal \mathcal{C}}(-, A) $$ $$ Hom(A,-): \ \mathcal{C} → Set $$

Hom-bifunctor: $$ Hom(-,-): \ \mathcal{C}^op × \mathcal{C} → Set $$

<<<Singleton>>>

SCHT: <2019-07-22 Mon>

Singleton - unit set - set with exactly one element. Also 1-tuple.

<<<Shadowing>>>

SCHT: <2019-07-28 Sun>

Global scope variable overriden by variable in local scope.

<<<Shrinking>>>

Process of reducing coplexity in the test case - re-run with smaller values and make sure that the test still fails.

<<<Smart constructor>>>

SCHT: <2019-07-24 Wed>

Place extra constraints on the construction of values.

<<<Spine>>>

SCHT: <2019-07-28 Sun>

Is a chain of memory cells, each points to the both value of element and to the next memory cell.

Array:

  :
 / \
1   :
   / \
  2   :
     / \
    3  []

1:2:3:[]

Spine:
  :
 / \
_   :
   / \
  _   :
     / \
    _  []

<<<Statement>>>

SCHT: <2019-08-03 Sat>

Declarative expression that is true or false.

*

<<<Assertion>>> <<<Assertions>>>

<<<Predicate>>>

Assertion function that includes variable and results in true or false statement.

Notation: $$ P(x) $$ Application of argument yealds true or false predicate.

<<<Superclass>>>

Broader parent class.

<<<Syntatic sugar>>>

SCHT: <2019-08-01 Thu>

Artificial way to make language easier to read and write.

<<<System F>>>

Formalizes the notion of parametric polymorphism in programming languages. Differs from the simply typed Lambda calculus by the introduction of universal quantification over types.

*

<<<Girard–Reynolds polymorphic lambda calculus>>> <<<Girard-Raynolds>>>

<<<Tail call>>>

SCHT: <2019-07-22 Mon>

Final evaluation producing result of the function.

<<<Tensor>>>

SCHT: <2019-07-22 Mon>

Object existing out of planes, thus it can translate objects from one plane into another. They can be tried to be described with knowledge existing inside planes, but representation would always be partial. Tensor of rank 1 is a vector.

Translatioin with tensor can be seen as functors.

*

<<<Tensors>>> <<<Tensorial>>>

<<<Testing>>>

<<<Property testing>>>

Since property has a law, then family of that unit tests can be abstracted into the lambda function. And tests cases come from generator.

<<<Function property>>>

Property corresponds to the according law. In property testing you need to think additionally about generator and shrinking.

<<<Property testing types>>>

	Exhaustive	Randomized	Unit test (Single sample)
Whole set of values	Exhaustive property test	Randomised property test
Special subset of values	Exhaustive specialised property test	Randomised specialised property test

<<<Generator>>>

Seed
|
v
Gen A -> A
^
|
Size

Seed allows reproducibility. There is anyway a need to have some seed. Size allows setting upper bound on size of generated value. Think about infinity of list.

After failed test - shrinking tests value parts of contrexample, finds a part that still fails, and recurses shrinking.

*

<<<Generators>>>

Custom generator

When sertain theorem only works for a specific set of values - the according generator needs to be produced.

arbitrary :: Arbitrary a => Gen a
suchThat :: Gen a -> (a -> Bool) -> Gen a
elements :: [a] -> Gen a

<<<Reusing test code>>>

Often it is convinient to abstract testing of same function properties:

It can be done with (aka TestSuite combinator):

-- Definition
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
eqSpec :: forall a. Arbitrary a => Spec

-- Usage
{-# LANGUAGE TypeApplications #-}
spec :: Spec
spec = do
  eqSpec @Int

Eq Int
  (==) :: Int -> Int -> Bool
    is reflexive
    is symetric
    is transitive
    is equivalent to (\ a b -> not $ a /= b)
  (/=) :: Int -> Int -> Bool
    is antireflexive
    is equivalent to (\ a b -> not $ a == b)

<<<Test Commutative property>>>

Commutativity

:: Arbitrary a => (a -> a -> a) -> Property

<<<Test Symmetry property>>>

Symmetry

:: Arbitrary a => (a -> a -> Bool) -> Property

<<<Test Equivalence property>>>

Equivalence

:: (Arbitrary a, Eq b) => (a -> b) -> (a -> b) -> Property

<<<Test Inverse property>>>

:: (Arbitrary a, Eq b) => (a -> b) -> (b -> a) -> Property

<<<QuickCheck>>>

Target is a member of the Arbitrary type class. Target -> Bool is something Testable. This properties can be complex. Generator arbitrary gets the seed, and produces values of Target. Function quickCheck runs the loop and tests that generated Target values always comply the property.

Manual automation with QuickCheck properties

import Test.QuickCheck
import Test.QuickCheck.Function
import Test.QuickCheck.Property.Common
import Test.QuickCheck.Property.Functor
import Test.QuickCheck.Property.Common.Internal

data Four' a b = Four' a a a b
  deriving (Eq, Show)

instance Functor (Four' a) where
  fmap f (Four' a b c d) = Four' a b c (f d)

instance (Arbitrary a, Arbitrary b) ⇒ Arbitrary (Four' a b) where
  arbitrary = do
    a1 ← arbitrary
    a2 ← arbitrary
    a3 ← arbitrary
    b ← arbitrary
    return (Four' a1 a2 a3 b)

-- Wrapper around `prop_FunctorId`
prop_AutoFunctorId ∷ Functor f ⇒ f a → Equal (f a)
prop_AutoFunctorId = prop_FunctorId T

type Prop_AutoFunctorId f a
  = f a
  → Equal (f a)

-- Wrapper around `prop_AutoFunctorCompose`
prop_AutoFunctorCompose ∷ Functor f ⇒ Fun a1 a2 → Fun a2 c → f a1 → Equal (f c)
prop_AutoFunctorCompose f1 f2 = prop_FunctorCompose (applyFun f1) (applyFun f2) T

type Prop_AutoFunctorCompose structureType origType midType resultType
  = Fun origType midType
  → Fun midType resultType
  → structureType origType
  → Equal (structureType resultType)

main = do
  quickCheck $ eq $ (prop_AutoFunctorId ∷ Prop_AutoFunctorId (Four' ())Integer)
  quickCheck $ eq $ (prop_AutoFunctorId ∷ Prop_AutoFunctorId (Four' ()) (Either Bool String))
  quickCheck $ eq $ (prop_AutoFunctorCompose ∷ Prop_AutoFunctorCompose (Four' ()) String Integer String)
  quickCheck $ eq $ (prop_AutoFunctorCompose ∷ Prop_AutoFunctorCompose (Four' ()) Integer String (Maybe Int))

Write tests algorithm

Pick the right language/stack to implement features.
How expensive breakage can be.
Pick the right tools to test this.

<<<Thunk>>>

Value that is yet to be evaluated. Can be dragged around, until be lazily evaluated.

<<<Uncurry>>>

Replace number of functions with tuple of number of values

<<<Undefined>>>

SCHT: <2019-09-03 Tue>

Placeholder value that helps to do typechecking.

<<<Unit>>>

SCHT: <2019-07-22 Mon>

Value, type. Represents nothing. Empty tuple

()

<<<Variable>>>

A name for expression.

Haskell has immutable variables. Except when you hack it with explicit funсtions.

*

<<<Variables>>>

<<<Zero>>>

SCHT: <2019-07-30 Tue>

* is the value with which operation always yelds Zero value. $$ zero, n ∈ C : ∀ n, zero*n=zero $$

* is distinct from Identity value.

<<<Modular arithmetic>>>

System for integers where numbers wrap around the certain values (single - modulus, plural - moduli).

Example - 12-hour clock.

*

<<<Clock arithmetic>>>

<<<Property>>>

Something has a property in the real world, and in theory its property corresponds to the law/laws, axioms.

In Haskell under property/law most often properties of algebraic structures.

There property testing wich does what it says.

*

<<<Properties>>>

<<<Associative law>>>

Joined with common purpose.

$$ P(a,P(b,c)) ≡ P(P(a,b),c) \ | \ ∀ (a,b,c) ∈ S $$,

Etymology: Latin associatus past participle of associare ”join with”, from assimilated form of ad ”to” + sociare ”unite with”, from socius ”companion, ally” from PIE *sokw-yo-, suffixed form of root *sekw- ”to follow”.

*

<<<Associativity>>> <<<Associative>>>

<<<Left associative>>>

SCHT: <2019-07-24 Wed>

Same level expression parts in reality follow grouping from left to right. $$ (λ x . x)(λ y . y)z ≡ ((λ x . x)(λ y . y))z $$

<<<Basis>>>

SCHT: <2019-07-22 Mon>

$$ β\alphaσ\iotaς $$ - stepping

The initial point, unreducible axioms and terms that spawn a theory. AKA see Category theory, or Euclidian geometry basis.

<<<Commutativity>>>

$$ ∀ (a,b) ∈ S : \; P(a,b) ≡ P(b,a) $$

*

<<<Commutative>>> <<<Commutative law>>>

<<<Idempotence>>>

First application gives a result. Then same operation can be applied multiple times without changing the result. Example: Start and Stop buttons on machines.

*

<<<Idempotent>>> <<<Idempotency>>>

<<<Backpack>>>

On first compilation - * analyzes the abstract signatures without loading side modules, doing the type check with assumption that modules provide right type signatures, and process does not emitt any binary code. Storing the intermediate code in a special form that allows flexibily connect modules provided. That allows later to compile project with particular instanciations of the modules, major work being done by internal Cabal Backpack support and Backpack system that modifies the intermediate code to fit the module.

<<<Nullary>>>

Taking no entries; having the arity of zero. Having trivial domain.

<<<Arbitrary>>>

arbitrarius uncertain

Give definitions

<<<Commuting diagram>>>

<<<Const functor>>>

<<<Free object>>>

When this object/property autofollows from rules&axioms.

<<<Thin category>>>

<<<Identity type>>>

<<<Constant type>>>

<<<Gen>>>

<<<ST-Trick monad>>>

ST is like a lexical scope, where all the variables/state disappear when the function returns https://wiki.haskell.ohttps://www.schoolofhaskell.com/school/to-infinity-and-beyond/older-but-still-interesting/deamortized-strg/Monad/ST https://dev.to/jvanbruegge/what-the-heck-is-polymorphism-nmh

*

<<<ST-Trick>>>

<<<Lax monoidal functor>>>

<<<Tensorial strength>>>

<<<Strong monad>>>

<<<Either>>>

Allows to separate and preserve information about happened, ex. error handling.

*

<<<Either data type>>>

<<<Weak head normal form>>>

*

<<<WHNF>>>

<<<Function image>>>

*

<<<Image>>>

<<<Maybe>>>

<<<Inverse>>>

Inverse function
In logic: $$ P → Q ⇒ ¬ P → ¬ Q $$, & same for category duality.

<<<Inversion>>>

Is a permutation where two elements are out of order.
See Inverse

<<<Inverse function>>>

$$ fx → y ˆ ({fx → y})-1 = {1}x $$

* $$ \iff $$ function is bijective. Otherwise - partial inverse

<<<Inverse morphism>>>

SCHT: <2019-07-23 Tue>

$$ f ˆ g = 1^x, g ˆ f = 1^y $$.

<<<Invertible>>>

<<<Invertibility>>>

<<<Partial inverse>>>

* when function is now bijective. When bijective see inverse function.

<<<Define LANGUAGE pragma options>>>

<<<ExistentialQuantification>>>

<<<GADTs>>>

<<<GeneralizedNewTypeClasses>>>

<<<FuncitonalDependencies>>>

<<<GHC debug keys>>>

<<<-ddump-ds>>>

Dump desugarer output.

*

<<<Desugar>>> <<<GHC desugar>>>

<<<GHC optimize keys>>>

<<<-foptimal-applicative-do>>>

$$ O(n^3) $$ Always finds optimal reduction into <*> for ApplicativeDo do notation.

<<<GHC check keys>>>

<<<-Wno-partial-type-signatures>>>

Supresses PartialTypeSignatures wildcard infer warning.

<<<Generalised algebraic data types>>>

LANGUAGE GADTs

*

<<<GADT>>>

<<<Order theory>>>

Investigates in thepth the intuitive notion of order using binary relations.

<<<Domain theory>>>

Formalizes approximation and convergense. Has close relation to Topology.

<<<Lattice>>>

Abstract structure that consists of partially ordered set, where every two elements have unique supremum and infinum. == * algebraic structure satisfying certain axiomatic identities. * order-theory & algebraic.

<<<Order>>>

<<<Preorder>>>

R^{X → X} : Reflexive & Transitive: $$ aRa $$ $$ aRb, bRc ⇒ aRc $$

Generalization of equivalence relations partial orders.

* Antisymmetric ⇒ Partial ordering. * Symmetric ⇒ Equivalence.

<<<Total preorder>>>

$$ ∀ a,b : a ≤ b ∨ b ≤ a $$ ⇒ Total Preorder.

<<<Partial order>>>

A binary relation must be reflexive, antisymmetric and transitive.

Partial - not every elempents between them need to be comparable.

Good example of * is a genealogical descendancy. Only related people produce relation, not related do not.

*

<<<Partial orders>>> <<<Partially ordered set>>> <<<Partially ordered sets>>> <<<Poset>>> <<<Posets>>>

<<<Partial order>>>

<<<Total order>>>

<<<Universal algebra>>>

Studies algebraic structures.

<<<Relation>>>

<<<Reflexivity>>>

$$ RX → X, ∀ x ∈ X : x R x $$ Order theory: $$ a ≤ a $$

* - each element is comparable to itself.

Corresponds to Identity and Automorphism.

*

<<<Reflexive>>> <<<Reflexive relation>>>

<<<Irreflexivity>>>

$$ RX → X, ∀ x ∈ X : \nexists R(x, x) $$

*

<<<Anti-reflexive>>> <<<Anti-reflexive relation>>> <<<Irreflexive>>> <<<Irreflexive relation>>>

<<<Transitivity>>>

$$ ∀ a,b,c ∈ X, ∀ RX → X : (aRb ∧ bRc) ⇒ aRc $$

* - the start of a chain of precedence relations must precede the end of the chain.

*

<<<Transitive>>> <<<Transitive relation>>>

<<<Symmetry>>>

$$ ∀ a,b ∈ X : (aRb \iff bRa) $$

*

<<<Symmetric>>> <<<Symmetric relation>>>

<<<Equivalence>>>

Reflexive	Symmetric	Transitive
$$ ∀ x ∈ X, ∃ R : x R x $$	$$ ∀ a,b ∈ X : (aRb \iff bRa) $$	$$ ∀ a,b,c ∈ X, ∀ R^{X → X} : (aRb ∧ bRc) ⇒ aRc $$
$$ a = a $$	$$ a = b \iff b = a $$	$$ a = b, b = c ⇒ a = c $$

*

<<<Equivalent>>> <<<Equivalent relation>>>

<<<Antisymmetry>>>

$$ ∀ a, b ∈ X : aRb, bRa ⇒ a = b $$ ~ $$ aRb, a ≠ b ⇒ \nexists bRa $$. Antisymmetry does not say anything about $$ R(a,a) $$.

* - no two different elements precede each other.

*

<<<Antisymmetric>>> <<<Antisymmetric relation>>>

<<<Asymmetry>>>

$$ ∀ a,b ∈ X (aRb ⇒ ¬ (bRa)) $$ * $$ \iff $$ Antisymmetric ∧ Irreflexive. Asymmetry ≠ “not symmetric” Symmetric ∧ Asymmetric is only empty relation.

*

<<<Asymmetric>>> <<<Asymmetric relation>>>

<<<Cryptomorphism>>>

Equivalent, interconvertable with no loss of information.

*

<<<Crypromorphic>>>

<<<Lexically scoped type variables>>>

Enable lexical scope for forall quantifier defined type variables

Implemented in ScopedTypeVariables

<<<Abstract data type>>>

Several definitions here, reduce them.

Data type mathematical model, defined by its semantics from the user point of view, listing possible values, operations on the data of the type, and behaviour of these operations.

* class of objects whose logical behaviour is defined by a set of values and set of operations (analogue to algebraic structure in mathematics).

A specification of a data type like a stack or queue where the specification does not contain any implementation details at all, only the operations for that data type. This can be thought of as the contract of the data type.

*

<<<AbsDT>>>

<<<ADT>>>

Abstract data type
Algebraic data type

<<<Concrete type>>>

SCHT: <2019-07-22 Mon>

Fully defined & non-polymorphic type.

<<<Functional dependencies>>>

<<<MonoLocalBinds>>>

<<<KindSignatures>>>

<<<ExplicitNamespaces>>>

<<<Combinator pattern>>>

<<<Symbolic expression>>>

Nested tree data structure. Introduced used in Lisp. In Lisp code and data are a *.

* in Lisp: Atom or expression of the form (x . y), x and y are *.

Modern abbriviated notation of *: (x y).

*

<<<S-expression>>> <<<S-expressions>>> <<<Sexpression>>> <<<Sexpressions>>> <<<Sexp>>> <<<Sexps>>> <<<Sexpr>>> <<<Sexprs>>>

<<<Polynomial>>>

Expression consisting of:

variables
coefficients
addition
substraction
multiplication (including positive integer variable exponentiation)

Polynomials forms a ring. Polynomial ring.

*

<<<Polynomials>>>

<<<Data family>>>

Indexed form of data and newtype definitions.

<<<Type synonym family>>>

Indexed form of type synonyms.

<<<Indexed type family>>>

* additional stucture in language that allows ad-hoc overloading of data types. AKA are to types as type class to methods.

Variaties:

data family
type synonym families

Defined by pattern matching the partial functions between types. Associates data types by type-level function defined by open-ended collection of valid instances of input types and corresponding output types.

Normal type classes define partial functions from types to a collection of named values by pattern matching on the input types, while type families define partial functions from types to types by pattern matching on the input types. In fact, in many uses of type families there is a single type class which logically contains both values and types associated with each instance. A type family declared inside a type class is called an associated type.

*

<<<Type family>>>

<<<TypeFamilies>>>

SCHT: <2019-07-17 Wed>

Allow use and definition of indexed type families and data families.

* are type-level programming. * are overload data types in the same way that type classes overload functions. * allow handling of dependent types. Before it Functional dependencies and GADTs were used to solve that. * useful for generic programming, creating highly parametrised interfaces for libraries, and creating interfaces with enhanced static iformation (much like dependent types).

Implies: MonoLocalBinds, KindSignatures, ExplicitNamespaces

Two types of * are:

<<<Error>>>

Mistake in the program that can be resolved only by fixing the program.

error is a sugar for undefined.

Distinct from Exception.

<<<Exception>>>

Expected but irregular situation.

Distinct from Error. Also see <<<Exception vs Error>>>

<<<ConstraintKinds>>>

SCHT: <2019-07-21 Sun>

Constraints are just handled as types of a particular kind (Constraint). Any type of the kind Constraints can be used as a constraint.

Anything which is already allowed in code as a constraint without *. Saturated applications to type classes, implicit parameter and equality constraints.
Tuples, all of whose component types have kind Constraint.

type Some a = (Show a, Ord a, Arbitrary a) -- is of kind Constraint.

Anything form of which is not yet known, but the user has declared for it to have kind Constraint (for which they need to import it from GHC.Exts):

Foo (f :: Type -> Constraint) = forall b. f b => b -> b -- is allowed
-- as well as examples involving type families:
type family Typ a b :: Constraint
type instance Typ Int  b = Show b
type instance Typ Bool b = Num b

func :: Typ a b => a -> b -> b
func = ...

<<<Propositional logic>>>

*

<<<Propositional calculus>>> <<<Statement logic>>> <<<Sentential logic>>> <<<Sentential calculus>>> <<<Zeroth-order logic>>>

<<<Second-order logic>>>

<<<Higher-order logic>>>

Citations

“One of the finer points of the Haskell community has been its propensity for recognizing abstract patterns in code which have well-defined, lawful representations in mathematics.” (Chris Allen, Julie Moronuki - “Haskell Programming from First Principles” (2017))

Good code

<<<Good: Type aliasing>>>

SCHT: <2019-07-23 Tue>

Use data type aliases to deferentiate logic of values.

<<<Good: Type wideness>>>

SCHT: <2019-07-22 Mon>

Wider the type the more it is polymorphic, means it has broader application and fits more types.

Concrete type fits only to itself.

The more constrained system has more usefulness.

Unconstrained means most flexible, but also most useless.

Parametric polymorphism is broader then constrained polymorphism

The widest type in current circumstances named principal type.

<<<Good: Read Conventions of variables (page 176)>>>

<<<Good: Print>>>

print :: Show a => a -> IO () print a = putStrLn (show a)

<<<Good: Read code evaluation (488 on-ward)>>>

<<<Good: Fold>>>

foldr spine recursion intermediated by the folding foldl spine folding is unconditional, then solding starts.

So foldr can terminate at any point, while foldl unconditionally recurses across the spine, even if it infinite.

<<<Good: Computation model>>>

SCHT: <2019-07-23 Tue>

Model the domain and types before thinking about how to write computations.

<<<Good: Make bottoms only local>>>

<<<Good: Newtype wrap is ideally transparent for compiler and does not change performance>>>

<<<Good: Instances of types/type classes must go with code you write>>>

<<<Good: Functions can be abstracted as arguments>>>

<<<Good: Infix operators can be bind to arguments>>>

<<<Good: Arbitrary>>>

SCHT: <2019-07-25 Thu>

Product types can be tested as a product of random generators. Sum types require to implement generators with separate constructors, and picking one of them, use `oneof` or `frequency` to pick generators.

<<<Good: Principle of Separation of concerns>>>

<<<Good: Function composition>>>

In Haskell inline composition requires:

h.g.f $ i

Function application has a higher priority than composition. That is why parentheses over argument are needed. This precedence allows idiomatically compose partially applied functions.

But it is a way better then:

h (g (f i))

<<<Good: Point-free>>>

Use Tacit very carefully - it hides types and harder to change code where it is used. Use just enough Tacit to communicate a bit better. Mostly only partial point-free communicates better.

<<<Good: Point-free is great in multi-dimentions>>>

SCHT: <2019-08-03 Sat>

BigData and OLAP analysis.

<<<Good: Functor application>>>

SCHT: <2019-07-23 Tue>

Function application on n levels beneath:

(fmap.fmap) function twoLevelStructure

How fmap.fmap typechecks:

(.)         :: (b -> c) -> (a -> b) -> a -> c
fmap        :: Functor f => (m -> n) -> f m -> f n
fmap        :: Functor g => (x -> y) -> g x -> g y

fmap . fmap :: (Functor f, Functor g)
              => ((g x -> g y) -> f . g x -> f . g y)
              -> ((  x ->   y) ->     g x  ->    g y)
              -> (   x ->   y) -> f . g x -> f . g y
fmap . fmap ::   (x    ->   y) -> f . g x -> f . g y

<<<Good: Parameter order>>>

In functions parameter order is important. It is best to use first the most reusable parameters. And as last one the one that can be the most variable, that is important to chain.

<<<Good: Applicative monoid>>>

There can be more then one valid Monoid for a data type. && There can be more than one valid Applicative instance for a data type. -> There can be differnt Applicatives with different Monoid implementations.

<<<Good: Creative process>>>

Pick phylosophy principles one to three the more - the harder the implementation

Draw the most blurred representation

Deduce abstractions and write remotely what they are

Model of computation

Model the domain

Model the types

Think how to write computations

Create

<<<Good: About operators (<$) (>) (<) (>>)>>>

SCHT: <2019-08-15 Thu>

Where character is not present - discards the according value.

<<<Good: About operators mapM_ sequence_>>>

Trailing _ means ignoring the result.

<<<Good: Guideliles>>>

Wiki.haskell

Documentation

Comments write in application terms, not technical.

Tell what code needs to do not how it does.

Haddoc

Put haddock comments to ever exposed data type and function.

Haddock header

{- |
Module      :  <File name or $Header$ to be replaced automatically>
Description :  <optional short text displayed on contents page>
Copyright   :  (c) <Authors or Affiliations>
License     :  <license>

Maintainer  :  <email>
Stability   :  unstable | experimental | provisional | stable | frozen
Portability :  portable | non-portable (<reason>)

<module description starting at first column>
-}

Code

Try to stay closer to portable (Haskell98) code

Try make lines no longer 80 chars

Last char in file should be newline

Symbolic infix identifiers is only library writer right

Every function does one thing.

<<<Good: Use Typed holes to progress the code>>>

Typed holes help build code in complex situations.

<<<Good: Haskell has infinite terms not not infinite types.>>>

That is why infinite types throw infinite type error.

<<<Good: Use type sysnonims to differ the information>>>

SCHT: <2019-07-26 Fri>

Even if there is types - define type synonims. They are free. That distinction with synonims, would allow TypeSynonymInstances, which would allow to create a diffrent type class instances and behaviour for different information.

<<<Good: Control.Monad.Error -> Control.Monad.Except>>>

<<<Good: Monad OR Applicative>>>

Start writing monad using ‘return’, ‘ap’, ‘liftM’, ‘liftM2’, ‘>>’ instead of ‘do’,’>>=’

If you wrote code and really needed only those - move that code to Applicative.

return -> pure
ap -> <*>
liftM -> liftA -> <$>
>> -> *>

Basic case when Applicative can be used

Can be rewriten in Applicative:

func = do
  a <- f
  b <- g
pure (a, b)

Can’t be rewritten in Applicative:

somethingdoSomething' n = do
a <- f n
b <- g a
pure (a, b)

(f n) creates monadic structure, binds ot to a wich is consumed then by g.

Applicative block vs Monad block

With Type Applicative every condition fails/succseeds independently. It needs a boilerplate data constructor/value pattern matching code to work. And code you can write only for so many cases and types, so boilerplate can not be so flexible as Monad that allows polymorphism. With Type Monad computation can return value that dependent from the previous computation result. So abort or dependent processing can happen.

<<<Good: Haskell Package Versioning Policy>>>

Version policy and dependency management.

*

<<<PVP>>> <<<Good: PVP>>>

<<<Good: Linear type>>>

Linear types are great to control/minimize resource usage.

<<<Good: Exception vs Error>>>

Many languages and Haskell have it all mixup. Here is table showing what belongs to one or other in standard libraries:

Exception	Prelude.catch, Control.Exception.catch, Control.Exception.try, IOError, Control.Monad.Error
Error	error, assert, Control.Exception.catch, Debug.Trace.trace

<<<Good: Let vs. Where>>>

let ... in ... is a separate expression. In contrast, where is bound to a surrounding syntactic construct (namespace).

Bad code

<<<Bad pragma>>>

Bad: Dangerous LANGUAGE pragma option

DatatypeContexts
OverlappingInstances
IncoherentInstances
ImpredicativeTypes
AllowAmbigiousTypes

Mine addition:

UndecidableInstances - often

Useful functions to remember

Prelude

enumFromTo
enumFromThenTo
reverse
show :: Show a => a -> String
flip
sequence - Evaluate each monadic action in the structure from left to right, and collect the results.
:sprint - show variables to see what has been evaluated already.
minBound - smaller bound
maxBound - larger bound
cycle :: [a] -> [a] - indefinitely cycle s list
repeat - indefinit lis from value
elemIndex e l - return first index, returns Maybe
fromMaybe (default if Nothing) e ::Maybe a -> a
lookup :: Eq a => a -> [(a, b)] -> Maybe b

Ord

compare

Calc

div - always makes rounding down, to infinity divMod - returns a tuple containing the result of integral division and modulo

List operations

concat - [ [a] ] -> [a]
elem x xs - is element a part of a list
zip :: [a] -> [b] -> [(a, b)] - zips two lists together. Zip stops when one list runs out.
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] - do the action on corresponding elements of list and store in the new list

Data.List

intersperse :: a -> [a] -> [a]  -  gets the value and incerts it between values in array
nub - remove duplicates from the list

Data.Char

ord (Char -> Int)
chr (Int -> Char)
isUpper (Char -> Bool)
toUpper (Char -> Char)

QuickCheck

quickCheck :: Testable prop => prop -> IO ()

quickCheck . verbose - run verbose mode

Investigate

Tools

ghc-pkg

List installed packages:

ghc-pkg list

Search over the Haskell packages code: Codesearch from Aelve

https://codesearch.aelve.com/

Integration of NixOS/Nix with Haskell IDE Engine (HIE) and Emacs (Spacemacs)

1. Install the Cachix: https://github.com/cachix/cachix

2. Install HIE on NixOS: https://github.com/infinisil/all-hies/#cached-builds

2.1. Cached builds

cachix use all-hies

2.2. NixOS installation:

{ config, pkgs, ... }:

let

  all-hies = import (fetchTarball "https://github.com/infinisil/all-hies/tarball/master") {};

in {
  environment.systemPackages = with pkgs; [

    (all-hies.selection { selector = p: { inherit (p) ghc865 ghc864; }; })

  ];
}

Insert your GHC versions.

2.3. Switch to new configuration:

sudo -i nixos-rebuild switch

3. Emacs (Spacemacs) configuration:

dotspacemacs-configuration-layers
'(

  auto-completion

  (lsp :variables
       default-nix-wrapper (lambda (args)
                             (append
                              (append (list "nix-shell" "-I" "." "--command" )
                                      (list (mapconcat 'identity args " "))
                                      )
                              (list (nix-current-sandbox))
                              )
                             )

       lsp-haskell-process-wrapper-function default-nix-wrapper
       )

  (haskell :variables
           haskell-enable-hindent t
           haskell-completion-backend 'lsp
           haskell-process-type 'cabal-new-repl
           )

)


 dotspacemacs-additional-packages '(
                                    direnv
                                    nix-sandbox
                                    )

Where:

auto-complettion configures YASnippet.

nix-sandbox (https://github.com/travisbhartwell/nix-emacs) has a great helper functions. Using nix-current-sandbox function in default-nix-wrapper that used to properly configure lsp-haskell-process-wrapper-function.

Configuration of the lsp-haskell-process-wrapper-function default-nix-wrapper is a key for HIE to work in nix-shell

Inside nix-shell the haskell-process-type 'cabal-new-repl is required.

Configuration was reassembled from: https://github.com/emacs-lsp/lsp-haskell/blob/8f2dbb6e827b1adce6360c56f795f29ecff1d7f6/lsp-haskell.el#L57 & its authors config: https://github.com/sevanspowell/dotfiles/blob/master.spacemacs /

Refresh Emasc.

4. Open the Haskell file from a project

Open system monitor, observe the process of environment establishing, packages loading & compiling.

5. Be pleased writing code

Now, the powers of the Haskell, Nix & Emacs combined. It’s fully in your hands now. Be cautious - you can change the world.

6. (optional) Debugging

If recieving sort-of:

readCreateProcess : cabal-helper-wrapper failure

HIE tries to run cabal operations like on the non-Nix system. So it is a problem with detection of nix-shell environment, running inside it.

If HIE keeps getting ready, failing & restarting - check that the projects ghc --version is declared in your all-hie NixOS configuration.

Debugger

Provides:

set a breakpoints
observe step-by-step evaluation
tracing mode

Breakpoints

:break 2
  :show breaks
  :delete 0
:continue

Step-by-step

:step main

List information at the breakpoint

:list

What been evaluated already

:sprint name

Libs

Exceptions

Exceptions - optionally pure extensible exceptions that are compatible with the mtl

Safe-exceptions - safe, simple API equivalent to the underlying implementation in terms of power, encourages best practices minimizing the chances of getting the exception handling wrong.

Enclosed-exceptions - capture exceptions from the enclosed computation, while reacting to asynchronous exceptions aimed at the calling thread.

Memory management

membrain - type-safe memory units

Parsers - megaparsec

CLIs - optparse-applicative

HTML - Lucid

Web applications - Servant

IO libraries

Conduit - practical, monolythic, guarantees termination return

Pipes + Pipes Parse - modular, more primitive, theoretically driven

JSON - aeson

Reference

<<<Functor-Applicative-Monad Proposal>>>

Well known historical even in Haskell: https://github.com/quchen/articles/blob/master/applicative_monad.md.

Math justice was restored with a RETroactive CONtinuity. Invented in computer science term Applicative (lax monoidal functor) become a superclass of Monad.

& that is why:

return = pure
ap = <*>
>> = *>
liftM = liftA = fmap
liftM* = liftA*

Also, a side-kick - Alternative became a superclass of MonadPlus. Hense:

mzero = empty
mplus = (<|>)

*

<<<Applicative-Monad proposal>>> <<<AMP>>>

Haskell-98

<<<Old instance termination rules>>>

∀ class constraint (C t1 .. tn): 1.1 type variables have occurances ≤ head 1.2 constructors+variables+repetitions < head 1.3 ¬ type functions (type func application can expand to arbitrary size)

∀ functional dependencies, ⟨tvs⟩_left → ⟨tvs⟩_right, of the class, every type variable in S(⟨tvs⟩_right) must appear in S(⟨tvs⟩_left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance head.

Liturgy

λειτ <- λαός Laos the people ουργός <- ἔργο ergon work λειτουργία leitourgia giving back to the community

The life is beautiful. For all humans that make the life have more uniqueness.

This study would not be possible without mathematicians, Haskellers, scientists, creators, contributors. These people are the most fascinating in my life.

Special accolades for the guys at Serokell. They were the force that got me inspired & gave resources to seriously learn Haskell and create this pocket guide.

Name		Name	Last commit message	Last commit date
Latest commit History 915 Commits
Book		Book
Good_code		Good_code
images		images
.gitignore		.gitignore
README.html		README.html
README.org		README.org
deeplists.tex		deeplists.tex

chengzh2008/haskell-notes

Folders and files

Latest commit

History

Repository files navigation

Introduction

Contents

Definitions

<<<Abstraction>>>

*

<<<Algebra>>>

*

<<<Algebraic>>>

<<<Algebraic structure>>>

*

<<<Alpha equivalence>>>

<<<Ambigram>>>

Ancient Greek and Latin prefixes

*

<<<Function application>>>

*

<<<Application memory>>>

<<<Argument>>>

<<<Argument of a function>>>

*

<<<As-pattern>>>

<<<Binary>>>

<<<Binary tree>>>

<<<Bind>>>

*

<<<Bottom value>>>

*

<<<Bound>>>

*

<<<Cartesian product>>>

*

<<<Case>>>

<<<Category theory>>>

*

<<<Abelian category>>>

<<<Composition>>>

*

<<<Endofunctor category>>>

<<<Functor>>>

*

<<<Power set functor>>>

<<<Power set functor laws>>>

*

<<<Power set functor identity law>>>

<<<Power set functor composition law>>>

<<<Lift>>>

*

<<<Power set functor is a free monad>>>

<<<Forgetful functor>>>

*

<<<Identity functor>>>

<<<Endofunctor>>>

*

<<<Applicative functor>>>

*

<<<Applicative laws>>>

<<<Applicative identity law>>>

<<<Applicative composition law>>>

<<<Applicative homomorphism law>>>

<<<Applicative interchange law>>>

<<<Applicative function>>>

<<<liftA*>>>

Conditional applicative computations

<<<Special applicatives>>>

<<<Identity applicative>>>

<<<Constant applicative>>>

<<<Maybe applicative>>>

<<<Either applicative>>>

<<<Validation applicative>>>

<<<Monad>>>

*

<<<Monad laws>>>

<<<Monad type class>>>

Functor -> Applicative -> Monad progression

<<<Monad function>>>