Introductory Course In Math: No Background Needed

1. Notion of representation
2. Notion of encoding
3. Requirements to glyphs: equality, recognisability, one might always realise where one ends and another begins
4. Deductive apparatus, mathematical theories
5. Interpretations of mathematical theories, constants
6. Variables, historic excursion into prop calc, difference between variables and constants; quantors; variable substitution and its pitfalls
7. What is Existence
8. What is Truth
9. Art of proof
10. Soundness, completeness, consistency
11. Proof theory
12. Model theory

(12 lessons, first two or three are short and may be conducted together)

Monadic Arithmetics

/* Stop >>= \a -> >>= \b insane! */

instance + (m a) | + a & Monad m
where
 (+) ma mb = ma >>= \a -> mb >>= \b -> return $! a + b

instance - (m a) | - a & Monad m
where
 (-) ma mb = ma >>= \a -> mb >>= \b -> return $! a - b

instance * (m a) | * a & Monad m
where
 (*) ma mb = ma >>= \a -> mb >>= \b -> return $! a * b

instance / (m a) | / a & Monad m
where
 (/) ma mb = ma >>= \a -> mb >>= \b -> return $! a / b

instance mod (m a) | mod a & Monad m
where
 (mod) ma mb = ma >>= \a -> mb >>= \b -> return $! a mod b

instance rem (m a) | rem a & Monad m
where
 (rem) ma mb = ma >>= \a -> mb >>= \b -> return $! a rem b

/* http://hpaste.org/10673 */

Heterogeneous lists for poor Concurrent Clean programmer

module sh /* search hlist */

import Same, FuncPipe, UnitType, UndefValue, Float, ErrorValue, Char, Logical, String
import Map, FPToolbox

Start = test2

//////////////////////////////

:: O = O
:: I a = I a

pos0 = O
add1 a = I a
add2 a = I (I a)
add3 a = I (I (I a))
pos1 = add1 pos0
pos2 = add2 pos0
pos3 = add3 pos0
pos4 = add1 pos3
pos5 = add2 pos4
pos6 = add3 pos3
pos7 = add3 pos4
pos8 = add3 pos5

///////////////////////////////////////////////////////

test2 :: String
test2 = selectHList pos0 ("hello",(-15.84,(100,(True,<>))))

class SelectHList i a t
where
 selectHList :: i a -> t

instance SelectHList (I i) (a,b) t | SelectHList i b t
where
 selectHList (I i) (a,b) = selectHList i b

instance SelectHList O (a,b) a` | Same a a`
where
 selectHList O (a,b) = same a

////////////////////////////////////////////////////

test :: String
test = searchHList ("hello",(-15.84,(100,(True,<>))))

class SearchHList t a
where
 searchHList :: !a -> t

instance SearchHList t <>
where
 searchHList <> = error "SearchHList: type not found!"

instance SearchHList t (a,b) | IfTypeEqual t a & SearchHList t b // allways inline this instance
where
 searchHList (a,b) = ifTypeEqual a $ searchHList b

class IfTypeEqual t a
where
 ifTypeEqual :: a t -> t

instance IfTypeEqual Int Int  where ifTypeEqual a b = a
instance IfTypeEqual Bool Bool  where ifTypeEqual a b = a
instance IfTypeEqual Float Float where ifTypeEqual a b = a
instance IfTypeEqual Char Char  where ifTypeEqual a b = a
instance IfTypeEqual String String where ifTypeEqual a b = a
instance IfTypeEqual [t] [a] | IfTypeEqual t a
where
 ifTypeEqual a b = map (\(ae,be) -> ifTypeEqual ae be) $ zip2 a b

instance IfTypeEqual t a where ifTypeEqual a f = f

My Desktop 2008

Laziness without laziness

foldM_ f xs = fold (\a e -> a >> f e) (return ()) xs

Instead of making chain of dynamically created functions from data list it is better to create a function that makes next function in chain

foldM_ f l = foldLoop l
where
        foldLoop []     = return ()
 foldLoop [x:xs] = f x >> foldLoop xs

Notice that this fragment does not use any language laziness.

2*n+h n Solution for Breadth-First Numbering (Okasaki paper)

data Tree a = Tree a (Tree a) (Tree a) | Leaf a | EmptyLeaf
 deriving (Show,Eq)

renameTreeNodes :: (Tree a) -> [Int] -> (Tree Int)
renameTreeNodes tree counts     = fst $ renameLoop tree counts
 where
 renameLoop EmptyLeaf   cs    = (EmptyLeaf, cs)
 renameLoop (Leaf _)   (c:cs)   = (Leaf c, (c+1):cs)
 renameLoop (Tree _ lb rb) (c:cs)   = (Tree c lb' rb', (c+1):csLR)
  where
  (lb',csL) = renameLoop lb cs
  (rb',csLR) = renameLoop rb csL

countsToBases :: [Int] -> [Int]
countsToBases cs = ctbLoop cs 1
 where
 ctbLoop [c] b  = [b]
 ctbLoop (c:cs) b = b:ctbLoop cs (b + c)

countOnEachLevel :: (Tree a) -> [Int]
countOnEachLevel tree = countLoop tree []
 where
 countLoop EmptyLeaf counts = counts
 countLoop (Leaf _) (c:cs) = (c+1):cs
 countLoop tree []  = countLoop tree [0]
 countLoop (Tree _ leftBranch rightBranch) (c:cs) = (c+1):csLR
  where
  csL = countLoop leftBranch cs
  csLR = countLoop rightBranch csL

---

Amazingly improved by BlackMeph

main = print . renameTreeNodes $ testTree

renameTreeNodes :: Tree a -> Tree Int
renameTreeNodes tree = t' where
    (t',ks) = renameLoop tree (1:ks)
    renameLoop EmptyLeaf cs = (EmptyLeaf,cs)
    renameLoop (Leaf _) (c:cs) = (Leaf c,(c+1):cs)
    renameLoop (Tree _ lb rb) (c:cs) = (Tree c lb' rb',(c+1):csLR) where
       (lb',csL)  = renameLoop lb cs
       (rb',csLR) = renameLoop rb csL

Source at HPASTE

Fascinating excursion in monads history

The notion of monad comes from category theory. It first arose in the area of homological algebra, but later was recognised (due to the work of Kleisli and of Eilenberg and Moore) to have much wider applications.

Its importance emerged slowly: in early days, it was not even given a proper name, but called simply a "standard construction" or a "triple". The formulation used here is due to Kleisli.

Eugenio Moggi proposed that monads provide a useful structuring tool for denotational semantics. He showed how lambda calculus could be given call-by-value and call-by-name semantics in an arbitrary monad, and how monads could encapsulate
a wide variety of programming language features such as state, exception handling, and continuations.

Independent of Moggi, but at about the same time, Michael Spivey proposed that monads provide a useful structuring tool for exception handling in pure functional languages, and demonstrated this thesis with an elegant program for term rewriting. He showed how monads could treat exceptions and non-deterministic choice in a common framework, thus capturing precisely a notion that I had groped towards years earlier.

Inspired byMoggi and Spivey, I proposed monads as a general technique for structuring functional programs. My early proposals were based on a special syntax for monads, that generalised list comprehensions. This was unfortunate, in that it led many to think a special syntax was needed.

This new presentation is designed to convey that monads can be profitably applied to structure programs today with existing languages.

A key observation of Moggi's was that values and computations should be assigned different types: the value type a is distinct from the computation type M a. In a call-by-value language, functions take values into computations (as in a -> M b); in a call-by-name language, functions take computations into computations (as in M a -> M b).

John Reynolds made exactly the same point a decade ago. The essence of Algol, according to Reynolds, is a programming language that distinguishes data types from phrase types. In his work data types (such as int) play the roles of values, and phrase types (such as int exp) play the role of computations, and the same distinction between call-by-value and call-by-name appears. These ideas form the basis for the design of Forsythe. But the vital unitM and bindM operations do not appear in Reynolds' work.

This is not the only time that John Reynolds has been a decade ahead of the rest of us. Among other things, he was an early promoter of continuation-passing style and the first to apply category theory to language design. One intriguing aspect of his recent work is the use of intersection types, so perhaps we should expect an upsurge of interest in that topic early in the next millenium.

-- "The essence of functional programming", Philip Wadler, University of Glasgow.