Re: Z_n in Haskell

[oleg]

The Z_n problem doesn't seem to be different from the problem of 
arrays or bitvectors of a statically-checkable size. 
If you prefer a decimal specification of the modulus, you may find the
following articles relevant. 

Implementation of fixed-precision decimal types:

Main> BV D1 0
Bitvector of width 1 and value 0
Main> BV (D1,D2) 123
Bitvector of width 12 and value 123
Main> BV (D5,D7,D9) 31415
Bitvector of width 579 and value 31415

It appears that modulus in the Z_n problem plays the same role as the
bitvector width in the bitvector problem.
An attempt to perform an operation on bitvectors of different sizes results
in a compiler error:

Main> (BV (D1,D0) 10) `b_and` (BV (D1,D1) 7)
ERROR - Type error in application
*** Expression : b_and (BV (D1,D0) 10) (BV (D1,D1) 7)
*** Term   : BV (D1,D0) 10
*** Type   : BitVector (D1,D0)
*** Does not match : BitVector (D1,D1)

http://groups.google.com/groups?selm=7eb8ac3e.0202201753.473a5cb2%40posting.google.com

Arbitrary precision decimal types, e.g.:

Main> BV (D1 $ D2 $ D3 $ D4 $ D5 $ D6 $ D7 $ D8 $ D9 $ D0 $ D9 $ D8 $
D7 $ D6 $ D5 $ D4 $ D3 $ D2 $ D1 $ Dim) 1234567879
Bitvector of width 1234567890987654321 and value 1234567879 

which are slightly more general and less convenient, are described in:

http://groups.google.com/groups?selm=7eb8ac3e.0202230221.62d98db8%40posting.google.com

Both implementations work in any Haskell-98 system. Multi-parameter
classes, existential types or other extensions are not needed.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Lambda over types.

[oleg]

anatoli  wrote:
> Attached are two interpreters: one for untyped lambda calculus,

I'm afraid the attached interpreter can't be an implementation of the
lambda calculus. For one thing, it lacks the hygiene of substitutions:

   Lambda> :t lambdaEval (A (L X (L Y (A X Y))) T)
   lambdaEval (A (L X (L Y (A X Y))) T) :: L Y (A T Y)   

That's OK. However,

   Lambda> :t lambdaEval (A (L X (L Y (A X Y))) Y)
   lambdaEval (A (L X (L Y (A X Y))) Y) :: L Y (A Y Y) 

That is wrong! The correct answer is: L Yfresh (A Y Yfresh)

The interpreter in question doesn't appear to be able to manufacture
fresh identifiers (i.e., fresh types). Without an ability to expand
the set of available identifiers, the capture-free substitution is
impossible.

Furthermore, some terms fail to evaluate:

   Lambda> :t lambdaEval (A (L X (A X X)) T)
   lambdaEval (A (L X (A X X)) T) :: Eval (A (L X (A X X)) T) a => a 

   Lambda> :t lambdaEval (A (A (L X X) T) Y)
   lambdaEval (A (A (L X X) T) Y) :: Eval (A (A (L X X) T) Y) a => a 

which is not the result one would've expected.

Finally, the interpreter doesn't actually find the normal form. The
rule 
   > instance Eval (L v e) (L v e)

prevents any reductions under lambda. True, call-by-name or
call-by-value interpreters stop short of reducing the body of a lambda
form. Normal or applicative order interpreters however -- in order to
find the beta-eta-normal form -- should seek and attempt any
reduction.

The hygienic substitution (with alpha-conversion if necessary) and the
repeated identification of the leftmost outermost redex are actually
quite challenging.

We can guarantee the hygienic substitution if we implement the de
Bruijin notation for lambda terms. Another, related technique is
coloring of existing identifiers. A macro-expander of R5RS Scheme
macros implements the coloring to ensure the hygiene of macro
expansions. The macro-expander can be cajoled into painting
identifiers on our demand, which has been used in a macro-expand-time
lambda calculator. In Haskell, we have to paint manually. A variable
in a typechecker-time lambda-calculator has to be represented by a
type like Vr (Succ (Succ (Succ Zero))) X. The latter component is the
"name" and the former is the color. The Eval and Subst relations
should be extended with color_in and color_out type parameters
(perhaps with a dependency: term color_in -> color_out). The only
non-trivial use of colors is in doing a substitution (L var
body)[exp/var']. The bound variable has to be repainted before the
substitution in the body. The beta-substitutor itself can do the
repainting.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Lambda over types.

[oleg]

anatoli  wrote:

> This is all, of course, of purely academical interest. The notation
> is extremely inconvenient to do any real work. I'd rather prefer
> a real, language-supported lambda over types.

> Or... wait a minute! You did find all those problems; does it mean
> you tried to *use* this stuff for something? Just curious.

I must start with a profuse apology, because what follows is perhaps
of little relevance to the list. I also propose to re-direct the
follow-ups to the Haskell Cafe.

I have examined your code and then tried a few examples, some of which
from my code's regression tests.

I have implemented a compile-time lambda-calculator, in a different
language. I should say, in a meta-language. The output of the
evaluator is a term that can then be compiled and evaluated. The
lambda-calculator acts as a partial evaluator. The calculator
normalizes a term in a pure untyped lambda calculus. The result is
compiled and evaluated in a call-by-value lambda-calculus with
constants.

Haskell typechecker (augmented with multi-parameter classes with
functional dependencies and let on loose) may do something similar.

BTW, the meta-language lambda-evaluator code (with the regression tests)
can be found at
    http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt
The calculator is implemented in CPS, in some sort of extended lambda
calculus. Therefore, the code has three kinds of lambdas: of the source
language, of the transformer meta-language, and of the target
language. The first and the third lambdas are spelled the same and
are the same.


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

trying to tie the knot

[oleg]

Hello!

Hal Daume III wrote:
[description of a parsing problem that involves forward references]

Forward references is the problem. To properly solve it, you have to
find a fixpoint. The best way to avoid hitting the bottom is to make
sure that the fixpoint combinator is applied to a function. Hence the
solution:

type TreeDictLate = [(String,DecisionTreeLate)] -- lookup for subtrees
newtype DecisionTreeLate = DTL (TreeDictLate -> DecisionTree)

ft (DTL late_tree) st = late_tree st

readDecisionTree :: String -> DecisionTree
readDecisionTree s = 
  let (_, wholeTreeLate, subTrees) 
  = readDecisionTree' False [] (filter (/=[]) (lines s))
  in ft wholeTreeLate subTrees

The function readDecisionTree' will return a delayed decision tree: a
function that _will_ yield the decision tree when it is applied to the
forest dictionary. The forest dictionary is itself an assoc list of
tree labels and _late_ decision trees.

Now the test "readDecisionTree $ unlines simpleDT3" passes as well,
and gives the reasonable result:

simpleDT3 = [
   "isArgument0 = t: u (33.0/1.4)",
   "isArgument0 = f:",
   "|   isArgument1 = f :[S1]",
   "|   isArgument1 = t:",
   "|   |   isRecursive1 = t: s (945.0/39.8)",
   "|   |   isRecursive1 = f: u (2.0/1.0)",
   "",
   "Subtree [S1]",
   "",
   "localDefCount <= 15 : u (281.0/1.4)",
   "localDefCount > 15 : s (139.0/11.8)"]


DecisionTree> readDecisionTree $ unlines simpleDT3

Test "isArgument0" "=" "t" (Value "u" 33.0 1.4)
  (Test "isArgument0" "=" "f"
(Test "isArgument1" "=" "f" 
  (Test "localDefCount" "<=" "15" (Value "u" 281.0 1.4) 
  (Value "s" 139.0 11.8))
  (Test "isArgument1" "=" "t"
(Test "isRecursive1" "=" "t" (Value "s" 945.0 39.8)
 (Value "u" 2.0 1.0))
(Value "" 0.0 0.0)))
 (Value "" 0.0 0.0)) 

which seems reasonable.

And even the following passes:
simpleDT4 = [
   "isArgument0 = t: u (33.0/1.4)",
   "isArgument0 = f:",
   "|   isArgument1 = f :[S1]",
   "|   isArgument1 = t :[S2]",
   "",
   "Subtree [S1]",
   "",
   "localDefCount <= 15 : [S2]",
   "localDefCount > 15 : s (139.0/11.8)",
   "",
   "Subtree [S2]",
   "",
   "ll <= 15 : u (2.0/1.4)",
   "ll > 15 : s (1.0/11.8)"]
readDecisionTree $ unlines simpleDT4
[skipped]

The code enclosed. BTW, it seemed the original code had a few bugs.

module DecisionTree where

import IO
import List

data DecisionTree = Test String String String DecisionTree DecisionTree | 
 Value String Double Double
 deriving (Show, Eq, Ord, Read)

type TreeDictLate = [(String,DecisionTreeLate)] -- lookup for subtrees
newtype DecisionTreeLate = DTL (TreeDictLate -> DecisionTree)

ft (DTL late_tree) st = late_tree st

readDecisionTree :: String -> DecisionTree
readDecisionTree s = 
  let (_, wholeTreeLate, subTrees) 
  = readDecisionTree' False [] (filter (/=[]) (lines s))
  in ft wholeTreeLate subTrees

readDecisionTree' :: Bool -> TreeDictLate -> [String] -> ([String],  DecisionTreeLate, 
TreeDictLate)

readDecisionTree' _ subTrees [] = ([], DTL $ \st -> Value "" 0 0, subTrees)

readDecisionTree' areValue subTrees (x:xs) =
   let (lineDepth, lineType, values') = readLine x
   (subTreesX,xs1) = if xs /= [] && "Subtree" `isPrefixOf` head xs
 then readSubTrees subTrees xs
 else (subTrees,xs)
   (xs',   lhs,   subTrees')   = readDecisionTree' False subTreesX  xs1
   (xs'' , rhs,   subTrees'')  = readDecisionTree' False subTrees' xs'
   (xs''', other, subTrees''') = readDecisionTree' True  subTreesX  xs1
   values = values' ++ ["0.0"]
   in  if lineType   -- are we a value
   then if areValue
then (xs1,DTL $ \st->Value (values !! 3) (read (values !! 4)) (read 
(values !! 5)), subTreesX)
else (xs''', DTL $ \st->Test (values !! 0) (values !! 1) (values !! 2) 
(Value (values !! 3) (read (values !! 4)) (read (values !! 5))) (ft other st), 
subTrees''')
   else if '[' == head (last values')   -- are we a subtree?
then (xs'', DTL $ \st-> 
let (Just dt) = lookup (last values') st
in Test (values !! 0) (values !! 1) (values !!2) (ft dt st) 
(ft lhs st), subTrees')
else (xs'', DTL $ \st->Test (values !! 0) (values !! 1) (values !! 2) (ft 
lhs st) (ft rhs st), subTrees'')

readSubTrees subTrees [] = (subTrees,[])

readSubTrees subTrees (x:xs)
| "Subtree" `isPrefixOf` x =
   let name = (words x) !! 1
   treeDef = takeWhile (\x -> not ("Subtree" `isPrefixOf` x)) xs
   rest= dropWhile (\x -> not ("Subtree" `isPrefixOf` x)) xs
   (_, thisDT, _) = readDecisionTree' False subTrees treeDef
   in  readSubTrees ((name,thisDT):subTrees) rest
| otherwise = (subTrees,(x:xs))

readLine :: String -> (Int,Bool,[String])  -- True = Value, False = Test
readLine s = (length 

ANN: Normal-order evaluation as bottom-up parsing

[oleg]

This message announces a normal-order lambda-calculator integrated
with Haskell. The calculator implements what seems to be an efficient
and elegant algorithm of normal order reductions. The algorithm is
"more functional" than the traditionally used approach. The algorithm
seems identical to that employed by yacc sans one critical difference.
The calculator also takes a more "functional" approach to the hygiene
of beta-substitutions, which is achieved by coloring of identifiers
where absolutely necessary. This approach is "more functional" because
it avoids a "global" counter or the threading of the paint bucket
through the whole the process. The integration with Haskell lets us
store terms in variables and easily and intuitively combine them. A
few examples (including 'greaterp', a term comparing two Church
numerals in magnitude) show how easy it is to program the calculator.

This message is an indirect reply to a recently posted query about the
treatment of free variables. The lambda-calculator in this message
shows one way of doing that.

The traditional recipe for normal-order reductions includes an
unpleasant phrase "cook until done". The phrase makes it necessary to
keep track of reduction attempts, and implies an ugly iterative
algorithm. We're proposing what seems to be efficient and elegant
technique that can be implemented through intuitive re-writing rules.
Our calculator, like yacc, possesses a stack and works by doing a
sequence of 'shift' and 'reduce' steps. We consider an application (a
b) as a _delayed_ normalization. We delay dealing with 'b' and with
the application until we figure out what to do with the term 'a'. The
calculator's stack contains all the terms to be applied to the current
one. The evaluator does a 'reduce' step when it is sure it has the
redex or it is sure it does not (e.g., (x (\y. y)) where 'x' is
free). When the evaluator is not sure about the current term, it
'shifts'. The only difference from yacc is that the lambda-calculator
"reparses" the result after the successful reduce step. The source and
the target languages of our "parser" (lambda-calculator) are the same;
therefore, the parser can indeed apply itself.

The evaluator's source code:
http://pobox.com/~oleg/ftp/Haskell/Lambda_calc.lhs

explains the algorithm in detail. The file has five times more lines
of comments than lines of code. The file also expounds upon the
hygiene of beta-substitutions achieved by "local painting".

The following are few examples:

First, we make a few variables.

> make_var = Var . VC 0  -- a convenience function
> [a,b,c,x,y,z,f,g,h,p,q] =
>map make_var ["a","b","c","x","y","z","f","g","h","p","q"]

If we type at the hugs prompt:
LC> eval $ (x ^ x # x) # (y ^ y # z)

we will see the answer "z z"
   
The substitutions are hygienic, as the following example demonstrates:
LC> eval $ a ^ (x ^ a ^ a # x) # (a # x)
==> (\a. (\a~1. a~1 (a x)))

A less trivial example (of integration with Haskell):

> c0 = f ^ x ^ x-- Church numeral 0
> succ = c ^ f ^ x ^ f # (c # f # x)-- Successor

> c1 = eval $ succ # c0   -- pre-evaluate other numerals
> c2 = eval $ succ # c1
> c3 = eval $ succ # c2
> c4 = eval $ succ # c3

It is indeed convenient to store terms in Haskell variables and
pre-evaluate (i.e., normalize) them. They are indeed terms. We can
always ask the interpreter to show the term. For example, "show c4"
yields "(\f. (\x. f (f (f (f x)".

> mul = a ^ b ^ f ^ a # (b # f) -- multiplication

Now, the interesting thing:
   eval $ mul # c1 ---> (\b. b), the identity function
   eval $ mul # c0 ---> (\b. (\f. (\x. x))), which is "const 0"

These are _algebraic_ results: multiplication of any number by zero is
always zero. Another algebraic result:
   eval $ zerop # (succ # a) ---> (\x. (\y. y)), that is, false.
Forall a, (succ a) is not zero. We can see now how lambda-calculus can
be useful for theorem proving (even over universally-quantified
formulas).

Finally, as even less trivial example, here is the term that compares two
Church numerals in magnitude. The example is excerpted from LC_neg.lhs
referenced below. The latter file provides all the definitions and a
long explanation.

> greaterp = eval $
>   a ^ b ^
>  -- Checking if anything is left of the list: if the current
>  -- cell is nil
> (car
>  # (b
>-- deconstructing the list. Once we hit the nil, we stop
># (z ^ lif # (car # z) # (cdr # z) # z)
>-- Building the list
># (a
>  # (z ^ (cons # true # z))
> 

Re: Bug in the scaling of randoms ...

[oleg]

Dimitre Novatchev wrote on May 4, 2002:
> In his excellent book Simon Thompson defines scaling of the elements of
> a sequence of random numbers from the interval [0, 65535] to an
> interval [s,t] in the following way (top of page 368):

> > scaleSequence :: Int -> Int -> [Int] -> [Int]
> > scaleSequence s t
> >   = map scale
> > where
> >   scale n = n `div` denom + s
> >   range   = t - s + 1
> >   denom   = modulus `div` range
> > where modulus = 65536
> However, the following expression:
>
> e4000 = (scaleSequence 1 966 ([65231] ++ [1..965]))!!0
> evaluates to 974 -- clearly outside of the specified interval.


Here's the algorithm for mapping of ranges of integers that is provably
correct. 

We aim to find a function sc(n) defined over integers 0 <= n <= M so
that
sc(0) -> s (given integral number)
sc(M) -> t (given integral number), t>=s
and
0<=a < b ==> sc(a) <= sc(b)

Such a function sc(n) is given by the following expression:
sc(n) = (n*(t-s)) `div` M + s

Proof:
sc(0) = s
sc(M) = (M*(t-s)) `div` M + s = t
a a*(t-s) < b*(t-s) ==> (a*(t-s)) `div` M <= (b*(t-s)) `div` M

The assertion that 0<=a a `div` M <= b `div` M for M >0 can
easily be proven by contradiction. Indeed, given the facts
(a `div` M)* M = a - ra, 0<= ra <= M-1
(b `div` M)* M = b - rb, 0<= rb <= M-1
and an assumption
a `div` M > b `div` M
we see
a = M*(a `div` M) + ra 
  = M*(b `div` M + x) + ra { where x >= 1 }
  = b - rb + ra + M*x
  >= min{ b - rb + ra + M*x over ra in [0,M-1], rb in [0,M-1]}
  >= b - (M-1) + M*x
  >= b + 1 + M*(x-1) { x >= 1 }
  >  b {contradiction}

Thus the correct algorithm reads

> scaleSequence :: Int -> Int -> [Int] -> [Int]
> scaleSequence s t
>   = map scale
> where
>   scale n = (n*range) `div` maxn + s
>   range   = t - s
>   maxn= modulus - 1
>   modulus = 65536

Given your example,
Main> any (==966) (scaleSequence 1 966 ([65231] ++ [1..965] ++[65565]))
True
Main> any (>966) (scaleSequence 1 966 ([65231] ++ [1..965] ++[65565]))
False 
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Proper scaling of randoms

[oleg]

This message derives an integer interval mapping function that is not
only provably within the given range but also "uniform". This is the
function to use when mapping random integers from one interval to a
smaller one.

Problem: given an integer n within [0..maxn], design a scaling
function sc(n) that returns an integer within [s..t], t>=s.
The function sc(n) must be 'monotonic': 
0<=a < b ==> sc(a) <= sc(b)
and it must map the ends of the interval:
sc(0) -> s and sc(maxn) -> t.

One such function has been designed by Simon Thompson in his book:
sct(n) = n `div` ((maxn+1) `div` (t-s+1)) + s

Another function has been derived in the previous message on this
list:
sc1(n) = (n*(t-s)) `div` maxn + s

The sct() function has a serious drawback: it is not guaranteed that
sct(n) <= t (more about it below). The sc1() function is provably
within the given range, and monotonic. Alas, it is not "uniform."

When it comes to mapping of random integers, the mapping function must
possess an extra property: it must "map uniformly." That is, given
random numbers within [0..maxn] such that Prob(n==i) - const, we must
aim at Prob(sc(n)==i') - const forall i' in [s..t]. The mapping
function sc1(n) does not have this property.

Any mapping function sc(n) from [0..maxn] to [s..t] for (t-s+1) <
(maxn+1) maps several integers from the source interval to one integer
of the target interval. An integer of the target interval therefore denotes an
equivalence class of the integers from the source interval.
The uniformity property will be satisfied only if the equivalence
classes have the same size. This is only possible if (maxn+1) `rem`
(t-s+1) == 0.

Given this condition, the original Thompson's algorithm works.  If
(t-s+1) divides (maxn+1) exactly (i.e., exists denom
integer. denom*(t-s+1) == maxn+1), we have
j*denom <= n <= j*denom+denom-1 ==> sct(n) = j+s, all j=0..(t-s) 
Thus each equivalence class has the size denom, and mapping is
perfectly uniform. As a consequence, s <= sct(n) <= t, given our
assumption (maxn+1) `rem` (t-s+1) == 0.

If this assumption does not hold, sct(n) may be greater than t (which
Dimitre Novatchev has demonstrated). Alas, in this case there is no
perfectly uniform mapping. The Thompson's algorithm misbehaves. The
worst case for the algorithm is when t = s + (maxn+1)/2. For example,
this occurs when we try to map [0..65535] to [0..32768]. In this case,
t-s+1 = 32769, and denom = 65536 `div` 32769 == 1, thus the mapping
becomes sct(n) = n. In almost half of the time, this mapping exceeds
the upper limit 32768.

OTH, the mapping sc1(n) = n*(maxn+1)/2 `div` maxn + s behaves in this
pathological case rather well. Not only sc1(n) <= t (this is always
guaranteed) but also the mapping is uniform: all equivalence classes
of the source interval [0..65535] except the last two classes have the
size of two.

Thus the best solution should be to "average" sc1(n) and sct(n).
This "averaging" is done by the formula
sca = (n*(t-s) + (n*(denom-1) `div` denom)) `div` maxn + s
where denom = (maxn+1) `div` (t-s+1)

It is easy to see that sca(0) -> s.
sca(maxn) = (maxn*(t-s) + (maxn*(denom-1) `div` denom)) `div` maxn + s
  = (maxn*(t-s) + p) `div` maxn + s
{where 0<= p = (maxn*(denom-1) `div` denom) <= maxn-1 }
  = t-s+s
  = t
It is easy to show that sca(n) is monotonic (as defined above).

If maxn+1 is evenly divisible by (t-s+1) (that is, denom*(t-s+1) ==
maxn+1), we have
j*denom <= n <= j*denom+denom-1 ==> sca(n) = j+s, all j=0..(t-s) 

This requires a proof.
We have:
sca(j*denom) 
  = (j*denom*(t-s) + (j*denom*(denom-1) `div` denom)) `div` maxn + s
  = (j*denom*(t-s) + j*(denom-1)) `div` maxn + s
  = j*(denom*(t-s) + denom-1) `div` maxn + s
  = j*maxn `div` maxn + s
  = j+s

sca(j*denom+denom-1) 
  = ((j*denom+denom-1)*(t-s) + ((j*denom+denom-1)*(denom-1) `div` denom)) `div` 
maxn + s
  = ((j*denom+denom-1)*(t-s) + (j+1)*(denom-1)-1) `div` maxn + s
  = (j*maxn + (denom-1)*(t-s+1)) `div` maxn + s
  = j+s
The required result then follows by the monotonicity property.

In the most pathological case of maxn= 65535, s=0, t= 32768.
We have denom = 1 and sca(n) becomes sc1(n), which, in this case,
behaves very well.

Thus the sca mapping is the optimal one. It is guaranteed to keep the
result within the specified bounds at all times. When the perfect
uniformity of mapping is possible, it is always achieved.

The implementation isn't too complex either.

> scaleSequence :: Int -> Int -> [Int] -> [Int]
> scaleSequence s t
>   = map scale
> where
>   scale n = (n*range + ((n*(denom-1)) `div` denom)) `div` maxn + s
>   range   = t - s
>   maxn= modulus - 1
>   modulus = 65536
>   denom   = (maxn+1) `div` (t-s+1)

Main> any(>966) (scaleSequence 1 966 [0..65535])
False
Main> any(==966) (scaleSequence 1 966 [0..65535])
True 
Main> any(>32768) (scaleSequence

Re: Pure File Reading (was: Dealing with configuration data)

[oleg]

There is another solution to the problem of configurational
parameters. The main part of the solution is portable, does not depend
on any pragmas, does not use unsafe operations, does not use implicit
parameters, and does not require any modifications to the user code. I
must warn that it is also potentially vomit-inducing.

It seems that the problem at hand naturally splits into two phases:
building the configuration environment, and executing some code in
that environment. The phases are executed sequentially. The facts
suggest the use of a SupedMonad. SuperMonad is very well known and
often used, even by people who never heard of simpler monads.

The following code is an illustration. Suppose file '/tmp/a.hs'
contains the following user code, which is to run within the
configuration environment provided by the module Config. For
simplicity, our configuration is made of one Int datum, config_item:

>>> File "/tmp/a.hs"

> import Config (config_item)
>
> foo = "foo shows: " ++ (show config_item)
>
> bar = "bar shows: " ++ (show config_item)
>
> main = do
>   print foo
>   print bar
>   print foo
  
We specifically illustrate the reading of the config item several
times.

The following code runs the first phase: reads the configuration,
build the SuperMonad and runs the SuperMonad.

> import System (system, ExitCode(ExitSuccess))
>
> myconfig_file = "/tmp/config"
>
> phaseII_var = "/tmp/Config.hs"
> phaseII_const = "/tmp/a.hs"
>
> nl = "\n"
>
> writeConfig :: Int -> IO ()
> writeConfig num = 
>   do
>writeFile phaseII_var $
> concat
>  ["module Config (config_item) where", nl,
>   "config_item =", show num, nl]
>  
>
> runSuperIO () = system ("echo main | hugs " ++ phaseII_const) 
> >>= \ExitSuccess -> print "Phase II done"
>  
> main = readFile myconfig_file >>= writeConfig . read >>= runSuperIO

I did warn you, didn't I?

I have a hunch this solution will work with GHC even better than it
works with Hugs. Perhaps we can even play with some dynamic linking
tricks (like shared object initializers, etc). BTW, the solution above
is similar in spirit to the following trick in C++:
Config config;
int main() { /* pure functional C++ code here -- yes, it exists*/}
the constructor for 'config' is guaranteed to run before main().

Perhaps someone will implement Staged Haskell one day?
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Q. about XML support

[oleg]

Joe English wrote:

> case nodeName node of
> "html:p" -> ...
> "html:h1" -> ...
> "html:pre" -> ...

> The approach I'm thinking of is to let the application programmer
> define an "internal" namespace environment, then rewrite
> element and attribute names in the parsed document to
> use the locally-defined prefixes.

SXML [1] treats the namespaces precisely this way. All element and
attribute names are fully resolved extended names, that is, with the
namespace URI if any, e.g.,
http://www.w3.org/1999/xhtml:p

All the names are symbols (a.k.a. interned strings), which means that
multiple occurrences of the same seemingly long name share all of the
name's characters. However, it is still awkward to read such
names. Therefore, SXML provides for so-called user ns-shortcuts. They
look like XML Name prefixes, with an important distinction:
ns-shortcuts are in a one-to-one correspondence with the namespace
URIs. XML Namespace prefixes do not have this property. Furthermore,
ns-shortcuts are determined by the author of the processing
application whereas XML Namespace prefixes are chosen by the author of
a document.

SXML specification discusses the issue of XML Namespaces in XML AST at
great length -- and points out to more discussion, about dealing with
namespaces in XPath and XSLT.

Incidentally, SXML is a language-neutral specification. One can easily
use Expat to write SXML. There are parsers that convert XML and a
(possibly ill-formed) HTML to SXML.

An example code [2] demonstrates parsing and unparsing of a
namespace-rich document: a DAML RDF file. DAML (DARPA Agent Markup
Language) ontologies typically use a great number of namespaces. The
example code demonstrates that
parse . unparse . parse === parse

[1] http://pobox.com/~oleg/ftp/Scheme/SXML.html

[2] http://cvs.sf.net/cgi-bin/viewcvs.cgi/ssax/SSAX/examples/daml-parse-unparse.scm
(written in Scheme, sorry)
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: fundeps for extended Monad definition

[oleg]

Hello!

Simon Peyton-Jones wrote:

> class C a b | a -> b where {}

> instance C Int Int where {}

> f1 :: (forall b. (C Int b) => Int -> b)
> f1 x = undefined

Indeed, this gives an error message 
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: Int
Inferred type: b

The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) => Int -> b)

Alas, 'exists' is not an allowed type quantifier. Not explicitly that
is. We can get 'exists' if we use the permitted 'forall' in a negative
position (aka in an existential type).

The following code

> class C a b | a -> b where {}

> instance C Int Int where {}

> newtype M a = M (forall b.(C a b) => b)
> f :: Int -> M Int
> f x = M undefined

typechecks in both Haskell compilers.

Hal Daume's original example works as well:

> newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
   

> class Monad2 m a ma | m a -> ma, ma -> m a where
>   return2 :: a -> ma
>   bind2   :: ma -> (a -> (MM2 m a)) -> (MM2 m a)
>   unused :: m a -> ()
>   unused  = \_  -> ()

> instance Monad2 [] a [a] where
>bind2 = error "urk"

Again, it typechecks both in Hugs and GHC.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: fundeps for extended Monad definition

[oleg]

Hello!

It seems we can truly implement Monad2 without pushing the
envelope too far. The solution and a few tests are given below. In
contrast to the previous approach, here we lift the type variables
rather than bury them. The principle is to bring the type logic
programming at the level of classes and instances but avoid putting
them at the level of their members.


> class TwoMonadific m a ma | m a -> ma, ma -> m a where
>   unused :: m a -> ()
>   unused = undefined
  
> instance TwoMonadific [] a [a]

> instance TwoMonadific Maybe a (Maybe a)

> class (TwoMonadific m a ma, TwoMonadific m b mb) => Monad2 m a b ma mb 
>  where
>   return2 :: a -> ma
>   bind2   :: ma -> (a -> mb) -> mb  

> instance Monad2 [] a b [a] [b] where
>   return2 x = [x]
>   bind2 l f = concatMap f l

> instance Monad2 Maybe a b (Maybe a) (Maybe b) where
>   return2 x = Just x
>   bind2 Nothing f = Nothing
>   bind2 (Just x) f = f x
  
> test1 = (return2 5) `bind2` (\n -> [1..n]) `bind2` (\n -> [1..n])

> test2 = (return2 5) `bind2` Just `bind2` Just

> *Main> test1
> [1,1,2,1,2,3,1,2,3,4,1,2,3,4,5]
> *Main> test2
> Just 5

It all works in GHC. Hugs complaints about return2:

  ERROR "/tmp/b.hs":11 - Ambiguous type signature in class declaration
  *** ambiguous type : Monad2 a b c d e => b -> d
  *** assigned to: return2

My version of Hugs isn't up-to-date though.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: fundeps for extended Monad definition

[oleg]

| > The reason, which is thoroughly explained in Simon Peyton-Jones'
| > message, is that the given type signature is wrong: it should read
| > f1 :: (exists b. (C Int b) => Int -> b)

> Can you give an example of its use?

Yes, I can.

> class (Show a, Show b) => C a b | a -> b where
> doit:: a -> b -> String
   
> instance C Int Int where
>doit a b = (show a)

> instance C Bool Bool where
>doit a b = if a then "everything" else "nothing"

> newtype M a = M (forall b.(C a b) => b)
> f :: Int -> M Int
> f x = M undefined

> g :: Bool -> M Bool
> g x = M undefined

> test1 a = case (f a) of
> M b -> doit a b

> test2 a = case (g a) of
> M b -> doit a b

I wonder if the Obfuscated Haskell contest has an entry for the most
useless type (with no uses). However, if a type can be used for the
contest, it is no longer the most useless. This makes one wonder if
the rules of the contest implicitly contain the Russel paradox.


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

First-class types

[oleg]

The following is a more flexible alternative to overloading. We
essentially define a function on types and invoke it, seemingly at run
time. No Dynamics or unsafe computations are employed. We only need
existential types, multi-parameter classes and functional
dependencies. The code also shows how to manipulate values which
cannot be manipulated.

As an example, we define a _function_ (not a method!) 'add' such that:

Main> add True False 
1
Main> add () (5::Int)
5
Main> add () (5::Float)
5.0
Main> add (4::Int) True
5
Main> add (10::Int) (5::Float)
15.0

The example works both in GHC and Hugs. The signature of add is quite
revealing:
forall b a2 a1.
(Num b, Coerce a2 b, Coerce a1 b, D a1 a2 b) =>
a1 -> a2 -> b

That is, 'add' is capable of adding any two _things_, provided they both can
be "generalized" and "coerced" into a number. The "type function" D
computes the generalization of two types -- in a manner we specify.

The function add is actually quite simple:

> add x y = let general_type = typeof x y
>   x' = coerce x general_type
>   y' = coerce y general_type
> in x' + y'

The function 'typeof' is also interesting. It has a type
forall b a2 a1. (D a1 a2 b) => a1 -> a2 -> b
Note that it returns 'b' forall b! In a sense, the function performs a
type computation at run time.

The code follows. We should note that we could have achieved the same
effect by defining an appropriate class with the method 'add'. In our
solution however, the acts of generalizing, coercion, and addition are
all separated. If we later decide to subtract things rather than add
them, we do not need to alter the class and all the instances. We
merely need to introduce the subtraction function. This makes the
maintenance of the code easier.

The distinct characteristic of the following code is an indirect
manipulation of an untouchable, existential value. We were able to
force a value to be of a specific type without any means of accessing
the value directly.

> class Type a where
> name :: a -> String

> instance Type Bool where
> name a = "Bool"

> instance Type Int where
> name a = "Int"

> --instance Type Char where
> --name a = "Char"

> instance Type () where
> name a = "()"

> instance Type Float where
> name a = "Float"

> -- Type generalization function: type -> type -> type
> class (Type b) => D a1 a2 b | a1 a2-> b
   
> instance D Bool Bool Int
> instance D Int Bool Int
> instance D Bool Int Int
> instance D Int Int Int
> instance D () Int Int
> instance D Int () Int
> instance D () () Int
> instance D Int Float Float
> instance D () Float Float
> instance D Float Int Float
> instance D Float Float Float

> -- The coercion function

> class Coerce a b where
> coerce :: a -> b -> b

> instance Coerce () Int where
> coerce _ _ = 0

> instance Coerce () Float where
> coerce _ _ = 0

> instance Coerce Int Int where
> coerce = const

> instance Coerce Float Float where
> coerce = const

> instance Coerce Int Float where
> coerce x _ = fromInteger $ toInteger x
   
> instance Coerce Bool Int where
> coerce True _ = 1
> coerce False _ = 0

> newtype M a1 a2 = M (forall b.(D a1 a2 b) => b)
> data M1 a1 a2 = M1 a1 a2 (M a1 a2)
> typeof v1 v2 = case (M1 v1 v2 (M undefined)) of M1 _ _ (M y) -> y
> typeof1 v1 v2 = case (M1 v1 v2 (M undefined)) of M1 _ _ y -> y

> add x y = let general_type = typeof x y
>   x' = coerce x general_type
>   y' = coerce y general_type
> in x' + y'
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: fundeps for extended Monad definition

[oleg]

Ashley Yakeley wrote:

> If this were allowed, it would effectively allow type-lambda
> class C a b | a -> b
> instance C Int Bool
> instance C Bool Char

> newtype T a = MkT (forall b.(C a b) => b)
> helperIn :: (forall b.(C a b) => b) -> T a
> helperIn b = MkT b; -- currently won't work
> helperOut :: T a -> (forall b.(C a b) => b)
> helperOut (MkT b) = b

And it does work (based on the code shown here previously):

> class C a b | a -> b
> instance C Int Bool
> instance C Bool Char
> instance C Char Float
> instance C Float (Int->())
> instance (C a b) => C (a->()) (b->())



> newtype T a = T (forall b.(C a b) => b)
> data T1 a = T1 a (T a) 
> xx b = case (T1 b (T undefined)) of T1 _ (T x) -> x


Ok, modules loaded: Main.
*Main> :type xx$(1::Int)
Bool
*Main> :type xx$ xx$ (1::Int)
Char
*Main> :type xx$ xx$ xx$ (1::Int)
Float
*Main> :type xx$ xx$ xx$ xx$ (1::Int)
Int -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ (1::Int)
Bool -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
Char -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
Float -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Int -> ()) -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Bool -> ()) -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Char -> ()) -> ()

It seems it does compute

The principle was to use constraints to force the "evaluation" of the
type "lambda". Obtaining the type "lambda" was the thrust behind the
exercise with existential and useless types. Perhaps I neglected to
mention that point.

We can use the Coerce type function (aka class) mentioned in the
thread on first-class types to convert from the types computed by 'xx'
to values. Incidentally, the class D was already a type function: the
function 'meet'.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Random Permutations

[oleg]

> 1. Generate N random numbers r_k, say, uniform between 0 and 1.
> 2. Form N pairs (1,r_1), (2,r_2), (3, r_3) ... (N,r_n).
> 3. Sort this list/vector wrt the *secon* (random) number.
> 4. In the sorted list the firs values (indices) give you the result.

> This is of course quite general, not restricted to any Haskell
> peculiarities.

I'm sorry but this algorithm does NOT in general provide the perfect
random permutation. Here's an excerpt from

    http://pobox.com/~oleg/ftp/Haskell/perfect-shuffle.txt
that deals extensively with this issue:

A commonly used shuffle algorithm attaches random tags to elements
of a sequence and then sorts the sequence by the tags. Although this
algorithm performs well in practice, it does not achieve the perfect
shuffling. 
 
Let us consider the simplest example (which happens to be the worst
case): a sequence of two elements, [a b]. According to the
shuffle-by-random-keys algorithm, we pick two binary random numbers,
and associate the first number with the 'a' element, and the second
number with the 'b' element. The two numbers are the tags (keys) for
the elements of the sequence. We then sort the keyed sequence in the
ascending order of the keys. We assume a stable sort algorithm. There
are only 4 possible combinations of two binary random
numbers. Therefore, there are only four possible tagged sequences:
[(0,a) (0,b)]
[(0,a) (1,b)]
[(1,a) (0,b)]
[(1,a) (1,b)]
After the sorting, the sequences become:
[(0,a) (0,b)]
[(0,a) (1,b)]
[(0,b) (1,a)]
[(1,a) (1,b)]
As we can see, after the sorting, the sequence [a, b] is three times
more likely than the sequence [b, a]. That can't be a perfect shuffle.

Furthermore, if we have a sequence of N elements and associate with
each element a key -- a random number uniformly distributed within [0,
M-1] (where N!>M>=N), we have the configurational space of size M^N
(i.e., M^N ways to key the sequence). There are N! possible
permutations of the sequence. Alas, for N>2 and Mhttp://www.haskell.org/mailman/listinfo/haskell

redefining methods in a subCLASS

[Oleg]

Hi

(Posted this to Haskell-Cafe 12 hours ago with no replies)

Is it possible to redefine methods in a subclass (not an instance)? E.g. I get 
errors in

class (Show a) => Employee a where
  speak :: a -> [Char]
  speak x = "Employee: " ++ (show x)

class (Employee a) => Manager a where
  speak x = "Manager: " ++ (show x)

Thanks
Oleg
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Class or parameterized type?

[oleg]

Hello!

> Example: I wish to define a structured container type, let's call it a 
> "RatsNest", that is type-variable in two ways:

> (a) it is parameterized by a type of some class, let's call it "RatsTail", 
> such that a RatsNest is a structure of things that have common 
> properties.  Certain operations between RatsNest values (e.g. a merge) are 
> valid only if they are containers for the same kind of RatsTail.  Such 
> operations would not be different operations due to variation of thye 
> contained type.

> (b) it can be implemented in various ways;  e.g. a simple version is an 
> in-memory data structure, while another may be implemented in database 
> storage.  This corresponds to the Haskell idea of overloading, or classes.

Do you consider the standard design lacking? For example,

-- sort of things to put into a RatNest
class (Eq n) => RatTail n where
is_the_same_rat:: n -> n -> Bool

class (RatTail t) => RatNest c t where
in_nest:: c t -> t -> Bool
put:: c t -> t -> c t
rat_fold:: (t -> z -> z) -> z -> (c t) -> z
merge:: (RatNest c1 t) => c t -> c1 t -> c t
merge c c1 = rat_fold put_perhaps c c1
   where put_perhaps rat nest = if in_nest nest rat then nest
else put nest rat

instance RatTail Int where
is_the_same_rat = (==)

-- Pretend this is an in-memory implementation
instance (RatTail t) => RatNest [] t where
in_nest lst el = not $ null $ filter (is_the_same_rat el) lst
put = (flip (:))
rat_fold = foldr

-- Pretend this is a "disk" implementation
-- At least it's unmarshalled.
newtype Disk t = D String deriving Show

instance (Read t, Show t, RatTail t) => RatNest Disk t where
in_nest disk el 
= rat_fold (\item z -> z || is_the_same_rat item el) False disk
put (D block) item = D $ '|' : ((show item) ++ block)
rat_fold f z (D []) = z
rat_fold f z (D ('|':block)) = f item $ rat_fold f z (D rest)
 where  [(item,rest)] = readsPrec 1 block

nest1 = [1,12,123] :: [Int]
nest2 = D ""
test1 = merge nest2 nest1 -- D "|1|12|123"
test1' = merge test1 nest1 -- D "|1|12|123"
test2 = merge [4,5,123] test1 -- [1,12,4,5,123]

Haskell extensions are required, of course, because we use
multi-parameter type classes.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Class or parameterized type?

[oleg]

Hello!

> I wasn't aware there was a standard design,
Edison is a good standard (in particular, Collection.hs, found, for
example, in /usr/local/share/hugs/lib/exts/).
The following projects have a lot of helpful code:

http://sourceforge.net/projects/hbase/
http://sourceforge.net/projects/hfl/

> [[
> class (RatTail t) => RatNest c t where
> ]]

> which I think is exactly what I was looking for, and is not a Haskell 
> structure I've come across before.  (I assume that this form does not 
> indicate that RatNest... is a subclass of RatTail (as opposed to saying 
> (RatTail t) => RatNest t);  I certainly wouldn't want to have that.)

Indeed,
> class (RatTail t) => RatNest c t where

says that collections of a class RatNest have elements of a class
RatTail t: but collections themselves are not in the class
RatTail. Using the OOP slang (which I hate), RatNest has-a RatTail but
RatNest is-not-a RatTail. The method is_the_same_rat applies, in
general, only to the elements of a RatNest, but not to the nest itself.


Nothing prevents us from declaring a particular instance of a RatNest
to be an instance of a RatTail as well. We can then store those
instances in a RatNest.

Nothing prevents us from making any RatNest a RatTail, so we can
always store nests inside nests.

-- sort of things to put into a RatNest
-- Unlike the code in the previous message, 
-- this class declaration does not have the Eq context
class RatTail n where
is_the_same_rat:: n -> n -> Bool

class (RatTail t) => RatNest c t where
in_nest:: c t -> t -> Bool
put:: c t -> t -> c t
rat_fold:: (t -> z -> z) -> z -> (c t) -> z
merge:: (RatNest c1 t) => c t -> c1 t -> c t
merge c c1 = rat_fold put_perhaps c c1
   where put_perhaps rat nest = if in_nest nest rat then nest
else put nest rat

instance RatTail Int where
is_the_same_rat = (==)

-- Pretend this is an in-memory implementation
instance (RatTail t) => RatNest [] t where
in_nest lst el = not $ null $ filter (is_the_same_rat el) lst
put = (flip (:))
rat_fold = foldr

-- Pretend this is a "disk" implementation
-- At least it's unmarshalled.
newtype Disk t = D String deriving Show

instance (Read t, Show t, RatTail t) => RatNest Disk t where
in_nest disk el 
= rat_fold (\item z -> z || is_the_same_rat item el) False disk
put (D block) item = D $ '|' : ((show item) ++ block)
rat_fold f z (D []) = z
rat_fold f z (D ('|':block)) = f item $ rat_fold f z (D rest)
  where  [(item,rest)] = readsPrec 1 block

nest1 = [1,12,123] :: [Int]
nest2 = D ""
test1 = merge nest2 nest1 -- D "|1|12|123"
test1' = merge test1 nest1 -- D "|1|12|123"
test2 = merge [4,5,123] test1 -- [1,12,4,5,123]

-- Every RatNest is a RatTail
instance (RatTail t, RatNest c t) => RatTail (c t) where
is_the_same_rat c1 c2 = subnest c1 c2 && subnest c2 c1
   where subnest c1 c2 
   = rat_fold (\item res -> in_nest c1 item && res) True c2
 
-- Now we can make nests of nests
test3 = merge [nest1] [test2] -- [[1,12,4,5,123],[1,12,123]]
test3' = merge [nest1] [nest1] -- [[1,12,123]]
test4 = put nest2 nest1 -- "|[1,12,123]"
test5 = merge test4 (put test4 test2) -- D "|[1,12,4,5,123]|[1,12,123]"
test7 = put [] test5 -- [D "|[1,12,4,5,123]|[1,12,123]"]

The test7 shows three nested nests.

> I suppose this is the multi-parameter type class extension you 
> mentioned.  Can you say where this extension is described, and how widely 
> implemented it is?

GHC (with the flag -fglasgow-exts) and Hugs (with the flag -98)
implement it. I think NHC does too.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: flock and sockets

[oleg]

John Hughes wrote:
> I didn't find this when I needed to lock files, so my solution (under
> Unix) was to write a little C code and call it via the FFI. I used a
> single lock file, since my application was a CGI script which runs fairly
> rarely -- there's no need for a finer grain of locking.

Many Linux/Unix systems come with 'procmail' installed. One part of that
installation is a nifty program called 'lockfile':

/tmp> lockfile -h
Usage: lockfile -v | -nnn | -r nnn | -l nnn | -s nnn | -! | -ml | -mu | file...
-v  display the version number and exit
-nnnwait nnn seconds between locking attempts
-r nnn  make at most nnn retries before giving up on a lock
-l nnn  set locktimeout to nnn seconds
-s nnn  suspend nnn seconds after a locktimeout occurred
-!  invert the exitcode of lockfile
-ml lock your system mail-spool file
-mu unlock your system mail-spool file

The man page is quite informative. The program is specifically
intended to be used in shell scripts. Therefore, we can use 'lockfile'
in any language system that is capable of executing a shell
command. In Hugs, we can use

> import System (system, ExitCode(ExitSuccess))
> do { system ("lockfile -ml") >>= \ExitSuccess -> print "OK" }

Therefore, we do not have to use FFI, we do not have to compile our
scripts. We can lock files right in Hugs or GHCi.

Daniel Luna wrote:
> The second option that I have is to use a daemon and let the programs that
> get started by mail connect via some sort of socket. Is there any socket
> support in Haskell?

One of the easiest ways of accomplishing this is by using inetd or
xinetd. In this case, your application _only_ needs to read from the
standard input and write into the standard output. An interactive
(that is, not a single request-single reply) daemon should also be
able to flush the standard output or set it to an unbuffered/line
buffered discipline. The application needs to know nothing at all
about sockets. Your network daemon could be just a (uncompiled)
Haskell code, interpreted by Hugs or GHCi.

For example, if you use inetd, you need to get your sysadm to add the
following line

mysrv   13720/tcp# my service, to listen on port 13720

into /etc/services and the following line

mysrv   stream tcp nowait yourname /home/you/daemon /home/you/daemon 

into /etc/inetd.conf and reHUP the inetd. The file /home/you/daemon
(with executable permissions set) is a start-up shell script

#!/bin/sh
cd /home/you/directory
PATH=right-path
exec hugs -flags your-script.lhs


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: simulating dynamic dispatch

[oleg]

> i'm hoping to be able to simulate a sort of dynamic dispatch based on
> class instances.

It seems you want to dispatch based not on a type but on the
constraint of a type. 

You code almost worked. Here's the a bit updated and working version.

class Foo a where { foo :: a -> Bool }
class Bar a where { bar :: a -> Bool }

data FB = forall a . Foo a => MkFoo a | forall a . Bar a => MkBar a

instance Foo FB where
foo (MkFoo x) = foo x

instance Bar FB where
bar (MkBar x) = bar x

-- some instances for the test
instance Foo Int where
foo x = x == 0

instance Bar Char where
bar x = x == 'a'


test x = case x of
  (MkFoo a) -> Just $ foo a
  (MkBar a) -> Just $ bar a
--_ -> Nothing


-- *Main> test $ MkFoo (0::Int)
-- Just True
-- *Main> test $ MkFoo (10::Int)
-- Just False
-- *Main> test $ MkBar 'a'  
-- Just True
-- *Main> test $ MkBar 'b'
-- Just False

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: simulating dynamic dispatch

[oleg]

Hal Daume wrote:
> -- *Main> test $ MkFoo (0::Int)
> -- Just True
> -- *Main> test $ MkBar 'a'  
> -- Just True

> i forgot to mention the constraint
> that i don't want the user to have to use the MkFoo/MkBar
> constructors.  if i could use them internally to 'test', that would be
> great, but that's what i couldn't get to work :).

It can be done without burdening the user with typing MkFoo and
MkBar. In fact, the enclosed code shows that it is possible to
implement the dynamic dispatch on a type class context -- exactly the
way you wanted it, it seems. The code resorts to no unsafe operations.

Here's the test:

-- *Main> test (1::Int)
-- "this is foo calling: 1"
-- *Main> test 'a'
-- "this is bar calling: 'a'"
-- *Main> test [True,False]
-- "this is quu calling: [True,False]"

Here's the code

-- Dynamic dispatch on a constraint: Foo, Bar, or Quux

-- The constraints to dispatch on

class Foo a where { foo :: a -> String }
class Bar a where { bar :: a -> String }
class Quu a where { quu :: a -> String }

-- Populate the type classes
instance Foo Int where
foo x = "this is foo calling: " ++ (show x)

instance Bar Char where
bar x = "this is bar calling: " ++ (show x)

instance Quu [Bool] where
quu x = "this is quu calling: " ++ (show x)


-- The Universe (with hidden constraints)
data PACK = forall a . Foo a => MkFoo a | forall a . Bar a => MkBar a
| forall a . Quu a => MkQuu a

-- The packer
class Packable a where
pack:: a -> PACK

-- The following three instances seem to be the "inverse"
-- of the "instance Foo Int" .. instance Quu [Bool]
-- The three instances below do an important job: they "introduce"
-- the class context, so to speak.
-- Also, a type can be a member of several type classes. The following
-- instances resolve the ambiguity. For example, even if Int were a member
-- of a class Bar (in addition to being the member of a class Foo), the first
-- instance declaration below resolves Int to a class Foo (and so we would
-- dispatch on Foo when we see an Int).

instance Packable Int where
pack = MkFoo

instance Packable Char where
pack = MkBar

instance Packable [Bool] where
pack = MkQuu

-- The dispatcher
instance Foo PACK where
foo (MkFoo x) = foo x

instance Bar PACK where
bar (MkBar x) = bar x

instance Quu PACK where
quu (MkQuu x) = quu x


test:: (Packable a) => a -> String
test = dispatch . pack
  where
dispatch x = case x of
  (MkFoo a) -> foo a
  (MkBar a) -> bar a
  (MkQuu a) -> quu a

-- *Main> test (1::Int)
-- "this is foo calling: 1"
-- *Main> test 'a'
-- "this is bar calling: 'a'"
-- *Main> test [True,False]
-- "this is quu calling: [True,False]"

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Polishing the boilerplate: a dis-unsafely safe cast

[oleg]

Hello!

The paper
http://research.microsoft.com/~simonpj/papers/hmap/
by Ralf Laemmel and Simon Peyton Jones gave a reference
implementation of a 'cast' function. Here's another implementation:

cast:: (Show a, Read b) => a -> Maybe b

cast = read_as . show
 where
   read_as s = case readsPrec 1 s of
[(r,[])] -> Just r
_-> Nothing

   
-- Tests from the hmap paper

-- *Main> (cast 'a') :: Maybe Char
-- Just 'a'
-- *Main> (cast 'a') :: Maybe Int 
-- Nothing
-- *Main> (cast 'a') :: Maybe Bool
-- Nothing
-- *Main> (cast True) :: Maybe Bool
-- Just True
-- *Main> (cast "True") :: Maybe Bool
-- Nothing
-- *Main> (cast "True") :: Maybe Int 
-- Nothing
-- *Main> (cast "True") :: Maybe String
-- Just "True"

-- Additional tests

-- *Main> (cast [1,2,3])::Maybe [Int]
-- Just [1,2,3]
-- *Main> (cast [1,2,3])::Maybe [Integer]
-- Just [1,2,3]
-- *Main> (cast [1,2,3])::Maybe [Float]
-- Just [1.0,2.0,3.0]
-- *Main> (cast (Just True)) :: Maybe Int
-- Nothing
-- *Main> (cast (Just True)) :: Maybe (Maybe Bool)
-- Just (Just True)
-- *Main> (cast (Nothing::Maybe Bool)) :: Maybe (Maybe Bool)
-- Just Nothing
-- *Main> (cast (Nothing::Maybe Bool)) :: Maybe (Maybe Int)
-- Just Nothing
-- *Main> (cast (Nothing::Maybe Bool)) :: Maybe (Maybe Char)
-- Just Nothing


Granted, the cast function here cannot handle exponential types. OTH,
the cast function given here can cast an Int to an Integer or to a Float. Most
of all, the cast function here is implemented entirely in Haskell 98,
with no extensions whatsoever -- not existential types, let alone
unsafeCoerce.


An aside: OCaml has a function called Obj.magic: 'a -> 'b,
which is unsafeCoerce with a positive name. If OCaml did not provide
that function, it can be easily emulated:

# let door_to_hell x =
 Marshal.from_string (Marshal.to_string () []) 0;;
val door_to_hell : 'a -> 'b = 

This is a terminating function with a signature a->b. It critically
relies on marshalling and unmarshalling. BTW, the function breaks all
kinds of free theorems:

#  let (fake_id: 'a->'a) = function x -> door_to_hell x;;
val fake_id : 'a -> 'a = 
# fake_id 123;;
- : int = 0

We can write a totally polymorphic terminating function a->a that is
patently not the identity.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Eval in Haskell

[oleg]

Simon Marlow wrote:

> The test driver makes use of 'eval'-style scripting, which none of the
> existing Haskell systems has.

Doesn't the following qualify as eval? A similar code works even in
Hugs.

> import System (system, ExitCode(ExitSuccess))
> import Posix(executeFile)
>
> myconfig_file = "/tmp/config"
>
> phaseII_var = "/tmp/Config.hs"
> phaseII_const = "/tmp/a.hs"
> phaseII_eval = "ghc --make "
> phaseII_result = "/tmp/a.out"
>
> nl = "\n"
>
> writeConfig :: Int -> IO ()
> writeConfig num =
>   do
>writeFile phaseII_var $
> concat
>  ["module Config (config_item) where", nl,
>   "config_item =", show num, nl]
>  
>
> runSuperIO () = system (phaseII_eval ++ 
> phaseII_const ++ " -o " ++ phaseII_result)
> >>= \ExitSuccess -> 
>  executeFile phaseII_result False [] Nothing
>
> main = readFile myconfig_file >>= writeConfig . read >>= runSuperIO

The context:
http://www.haskell.org/pipermail/haskell-cafe/2003-February/003912.html

Furthermore, if GHCi can (after some prodding by the user) launch ghc
to compile a module and then load the resulting .o file in and
apply some function in thus loaded file, doesn't it feel like an eval?

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Eval in Haskell

[oleg]

Tomasz Zielonka wrote:
> I don't know how it works in Python, but in perl the code in eval is
> executed in current lexical scope.

Eval of the kind
let x = 1 in eval "x"
is plainly an abomination. Such an eval all but precludes compilation
because the compiler is not free to alpha-rename lexical bindings any
more and cannot eliminate bindings by inlining. Incidentally, the eval
in Scheme does not (and cannot, in general) use let-bindings. Scheme's
eval may consult previously declared top-level bindings -- but only
given an appropriate flag (whose existence is entirely optional).

Incidentally, restricting eval to top-level or "standard" bindings is 
not a significant limitation. It is, in general, a very good practice
to apply eval to closed expressions only. For example, 
let x = 1 in (eval "\x->x") x
or
y = 1
main = (eval "let x = " ++ (show y) ++ " in x" ) >>= putStrLn
or (if we need to pass many parameters)
y = 1
z = 2
do
   writeFile "Conf.hs" $ makeBindings [["y", show y],["z", show z]];
   result <- eval "import Conf;y+z";
   putStrLn result

Thus if we restrict all parameters for eval to be in the class
Show/Read, we can implement such an eval right now.

P.S. It has crossed my mind to suggest Scheme as a driver for the
regression tests -- using Ashley Yakeley's HScheme system. I know of
several commercial projects that use Scheme to drive regression tests
for Java projects (Scheme being implemented in Java itself).
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Safe and sound STRef [Was Implementing RefMonads in Haskell without ST,IO]

[oleg]

Back in September 2001, Koen Claessen wrote:
] Here is a little experiment I did a while ago. I was trying to isolate
] the capability of the ST monad to deal with different types at the
] same time  I conjecture this functionality cannot be implemented
] in Haskell 98, nor in any of the known safe extensions of Haskell.

Recently, Tim Sweeney wrote
] Is it possible to actually implement a working instance of RefMonad in
] Haskell, without making use of a built-in monad like IO or ST?

The following code shows a safe and sound implementation of a
polymorphic heap with references and updates. The heap is capable of
storing of polymorphic, functional and IO values. All operations are
*statically* checked. An attempt to alter a heap reference with a
value of a mismatched type leads to a _compile-time_ error. Everything
is implemented in Haskell98 + multiparameter classes with functional
dependencies + overlapping instances. I suspect that the latter isn't
strictly needed, but it's almost midnight. Most importantly, no IO or
ST monad, no unsafePerformIO or unsafeCoerce, no existential types and
no Dynamics are needed. It seems that the polymorphic updateable heap
can be implemented safely. Although the code looks like a monadic
code, the Monad class doesn't seem to be polymorphic enough to wrap
our heap. Perhaps arrows will help.

I'd like to remark first that the ST monad with polymorphic STRef can
be implemented in Haskell98 + safe extensions _provided_ all the
values question are in the class Show/Read. When we store values,
we store their external representation. When we retrieve a value, we
read it. Similarly for values in the Binary class. All such values are
_safely_ coercible. The following code however does not make this
assumption. In our heap below, we can even store polymorphic
functions and IO values!


First, the tags for values in our heap

> data Zero
> data Succ a
>
> class HeapTag a where
> tag_value:: a -> Int
>
> instance HeapTag Zero where
> tag_value _ = 0
>   -- I just can't avoid the undefined arithmetics
> instance (HeapTag t) => HeapTag (Succ t) where
> tag_value _ = 1 + tag_value (undefined::t)

The heap reference is the combination of the tag and the desired
type. As we will see, the value of the second argument of the HeapRef
doesn't actually matter -- only its type does.

> data HeapRef t a = HeapRef t a

Our heap is implemented as a polymorphic associative list

> data Nil t v r  = Nil
> data Cons t v r = Cons t v r
>
> class PList ntype ttype vtype cdrtype where
> cdr::   ntype ttype vtype cdrtype -> cdrtype
> empty:: ntype ttype vtype cdrtype -> Bool
> value:: ntype ttype vtype cdrtype -> vtype
> tag::   ntype ttype vtype cdrtype -> ttype
>   
> instance PList Nil ttype vtype cdrtype where
> empty = const True
>
> instance (PList n t v r,HeapTag tag) => PList Cons tag vtype (n t v r) where
>  empty = const False
>  value (Cons t v r) = v
>  tag   (Cons t v r) = t
>  cdr   (Cons t v r) = r


The following is the statically typed polymorphic heap itself:

> class Heap t v h | t h -> v where
> fetch:: (HeapRef t v) -> h -> v
> alter:: (HeapRef t v) -> v -> h -> h
>  
> instance (HeapTag t,PList Cons t v r) => Heap t v (Cons t v r) where
> fetch _ p = value p
> alter _ vnew (Cons t v r) = (Cons t vnew r)
>
> instance (HeapTag t,Heap t v r,PList Cons t' v' r) => 
>  Heap t v (Cons t' v' r) where
> fetch ref p = fetch ref $ cdr p
> alter ref vnew (Cons t v r) = Cons t v $ alter ref vnew r

Let's make our heap instances of a class Show, so we have something to show.

> instance (PList Nil ttype vtype cdrtype) => Show (Nil ttype vtype cdrtype)
>where
> show _ = "[]"

> instance (Show vtype, HeapTag ttype, PList Cons ttype vtype cdrtype,
>   Show cdrtype) =>
> Show (Cons ttype vtype cdrtype)
>   where
> show x = (show $ (tag_value $ tag x, value x)) ++ " : " ++ (show $ cdr x)


Let's take a few simple examples

> tinc (x::t) = undefined::(Succ t)
> tag_one = (undefined::(Succ Zero))
> acons = Cons

> lst1 = acons tag_one 'a' $ Nil
> lst2 = acons (tinc tag_one) 'a' $ acons tag_one True $ Nil
> test1 = fetch (HeapRef tag_one 'z') lst1

The result is 'a'. We see that the value of the second argument of
HeapRef doesn't actually matter. But its type sure does: if we
uncomment the following line

> -- test1' = fetch (HeapRef tag_one (1::Int)) lst1

we get an error:

/tmp/o1.lhs:127:
Couldn't match `Char' against `Int'
Expected type: Char
Inferred type: Int
When using functional dependencies to combine
  Heap t v (Cons t v r),
arising from the instance declaration at /tmp/o1.lhs:91
  Heap (Succ Zero) Int (Cons (Succ Zero) Char (Nil t v r)),
arising from use of `fetch' at /tmp/o1.lhs:127
When generalising the type(s) for `test1''

Indeed, the stored value is of type Char and we try to read it as a

Re: Safe and sound STRef

[oleg]

> Heaps should be more dynamic than this; the (type of the) *reference*
> should encode the type it points to, but the (type of the) *heap*
> should not.

However, the heap can store polymorphic values. Therefore, we can use
a heap to store the polymorphic heap... Your example, slightly
re-written as follows, types

test5 = do
let heapi = init_gh
let (href,heap2) = alloc_gh undefined heapi
let (mr,heap1) = 
   if 1<2 then
   let (xr,h) = alloc_gh 42 heapi 
   heap2' = alter_gh href h heap2
   in (Just xr,heap2')
   else
   (Nothing,heap2)
print $
  case mr of
  Nothing -> ""
  Just r  -> show (fetch_gh r (fetch_gh href heap1))

and even prints the answer to everything...

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Typesafe MRef with a regular monad

[oleg]

It seems it is possible to implement polymorphic references using the
regular (not IO and not ST) monad and without resorting to any unsafe
extension. Furthermore, that monad has a run function, which does not
compromise the type safety.

When I claimed in the previous message that the polytypic nature of
the heap precludes its encapsulation in a monad, I was fortunately
mistaken. I was confused: I thought that a function signature a->a
meant that the type of the argument must be identical to the type of
the result. That is clearly not true: the type of the argument should
merely be specializable to the type of the result. If we pre-allocate
a heap with, say, 5 cells of the undefined value, we can store values
of any type in these cells. Of course, after we wrote something in a
cell, we can overwrite it with the value of the same or a more
specialized type. Therefore, we can seek the fixpoint heap without
offending the typechecker. This gives us a desired monad.


[Continuing the code from the original message]
A pre-allocated heap of 5 cells:

> t1 = tag_one
> t2 = (tinc t1)
> t3 = (tinc t2)
> t4 = (tinc t3)
> t5 = (tinc t4)
> heap5 = Cons t5 undefined $ Cons t4 undefined $ Cons t3 undefined $
> Cons t2 undefined $ Cons t1 undefined $ Nil


A Heap monad:

> newtype HeapM h a = HeapM (h->(a,h))
>
> instance Monad (HeapM h) where
>return x = HeapM $ \h -> (x, h)
>HeapM  m >>= f = HeapM $ \h -> let (x, h') = m h; HeapM m' = f x in m' h'


The argument of hget and hput functions below must be a heap of 5
cells, with arbitrary values. heap5 is the most general heap of that
sort

> hget tag = HeapM $ \(h::t) -> (fetch (HeapRef tag undefined) h,h)
>   where x::t = heap5
> 
> hput tag newval = HeapM $ 
>   \(h::t) -> ((),alter (HeapRef tag undefined) newval h)
>   where x::t = heap5

We can run our monad:

> runHOF (HeapM hf) = fst $ hf heap5

The test. We test storing and altering polymorphic values, including
polymorphic functional values!

> test7 = do
>  let l1 = tag_one 
>  hput l1 'a'
>  v1 <- hget l1
>
>  let l2 = tinc l1  -- our allocator is somewhat primitive at the moment
>  hput l2 Nothing   -- storing a polymorphic value of type Maybe a
>  v2 <- hget l2
>
>  let l3 = tinc l2
>  hput l3 (\x->x+1)  -- storing a polymorphic function over Num a
>  v3 <- hget l3
>
>  -- Update the cells and retrieve the updated values
>  hput l1 'b'
>  v11 <- hget l1
>  hput l2 $ Just True -- overwrite with a more specialized value
>  v21 <- hget l2
>  hput l3 (\x->x+5)
>  v31 <- hget l3
>  return $ [[show v1,  show v2,  show $ v3 1], 
>[show v11, show v21, show $ v31 1]]
   
The result is

*Main> runHOF test7
[["'a'","Nothing","2"],["'b'","Just True","6"]]


Ashley Yakeley wrote:
] ] Is it possible to actually implement a working instance of RefMonad in 
] ] Haskell, without making use of a built-in monad like IO or ST?  

] You certainly wouldn't be able to do this for any monad M which had:

]   performM :: forall a. M a -> a;

] ...because it wouldn't be type-safe: you'd be able to construct coerce 
] :: a -> b just as you can with unsafePerformIO.
 
Fortunately, that doesn't seem to be the case.  Here's an example that is
roughly  equivalent to the unsafe example in the documentation for
unsafePerformIO. Note that t1 is equivalent to readIORef [a] (actually,
t1  points out to a reference cell Ref a, which can accept values of
any type whatsoever).


--> test9 = do
-->  hput t1 []
-->  hput t1 [42]
-->  bang <- hget t1
-->  return $ (bang ::[Char])

If we uncomment the above code, we get a compiler error:

/tmp/o1.lhs:327:
No instance for (Num Char)
arising from the literal `42' at /tmp/o1.lhs:327
In the list element: 42
In the second argument of `hput', namely `[42]'


A nicer implementation of newRef (an allocator) is left for the future
work. I think that the pre-allocation trick makes it possible.

The pre-allocation scheme isn't such a limitation: clearly we can not
invoke newSTRef or newIORef arbitrary number of times (while keeping
the references). Sooner or later something unpleasant happens. We can
think therefore of newSTRef as indexing in a some pre-allocated array.
With the template Haskell, we can easily pre-allocate a heap of 640K
cells, and that should be enough for everybody.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Typesafe MRef with a regular monad

[oleg]

> update  :: (Typable b) => FM k -> Key k a -> b -> (FM ...)

I didn't know constraints on values are allowed... Given below is the
implementation of the required interface, in Haskell98

   module TypedFM where
data FM k -- Abstract; finite map indexed bykeys of type k
data Key k a  -- Abstract; a key of type k, indexing a value of type a
 
empty :: FM k
insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
lookup :: Ord k => FM k -> Key k a -> Maybe a
update :: Ord k => FM k -> Key k a -> a -> FM k


Implementation:

import Monad

data U =  LBool Bool 
| LChar Char
| LInt Int
| LL [U]  -- Lists of any kind
| LA (U->U) -- monomorophic functions of any kind


class UNIV a where
inj:: a -> U
prj:: U -> Maybe a


instance UNIV Bool where
inj = LBool
prj (LBool a) = Just a
prj _ = Nothing

instance UNIV Char where
inj = LChar
prj (LChar a) = Just a
prj _ = Nothing

instance UNIV Int where
inj = LInt
prj (LInt a) = Just a
prj _ = Nothing

instance (UNIV a) => UNIV [a] where
inj = LL . map inj
prj (LL as) = foldr f (Just []) as
where f e (Just s) = case prj e of
 Just x -> Just $ x:s
 _  -> Nothing
  f _ _ = Nothing
prj _ = Nothing

instance (UNIV a,UNIV b) => UNIV (a->b) where
inj f = LA $ \ua -> let (Just x) = prj ua in inj $ f x
prj (LA f) = Just $ \x -> let Just y = prj$f$inj x in y
prj _ = Nothing

data FM k = FM [U]

data Key k a = Key Int a

empty = FM []

insert (FM l) _ a = (FM $(inj a):l, Key (length l) a)

lookp:: (UNIV a) => FM k -> Key k a -> Maybe a
lookp (FM l) (Key i a) = prj $ (reverse l)!!i

update:: (UNIV a) => FM k -> Key k a -> a -> FM k
update (FM l) (Key i _) a = FM $ reverse (lb ++ ((inj a):(tail lafter)))
where (lb,lafter) = splitAt i (reverse l)

  
test1 = do
let heap = empty
let (heap1,xref) = insert heap () 'a'
let (heap2,yref) = insert heap1 () [(1::Int),2,3]
let (heap3,zref) = insert heap2 () "abcd"
putStrLn "\nAfter allocations"
--  print heap3

putStr "x is "; print $ lookp heap3 xref
putStr "y is "; print $ lookp heap3 yref
putStr "z is "; print $ lookp heap3 zref

let heap31 = update heap3  xref 'z'
let heap32 = update heap31 yref []
let heap33 = update heap32 zref "new string"
putStrLn "\nAfter updates"

putStr "x is "; print $ lookp heap33 xref
putStr "y is "; print $ lookp heap33 yref
putStr "z is "; print $ lookp heap33 zref

putStrLn "\nFunctional values"
let (heap4,gref) = insert heap33 () (\x->x+(1::Int))
putStr "g 1 is "; print $ liftM2 ($) (lookp heap4 gref) $ Just (1::Int)
return ()
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Typesafe MRef's

[oleg]

> So what does the function
> insert2 val1 val2 =
>let
>   (m1,k1) = insert empty (Just val1)
>   (m2,k2) = insert m1 (Just val2)
>   m3 = update m2 k1 Nothing
>in
>   isJust (lookup m3 k2)
> return?  It looks to me as if it returns True if val1 and val2 have
> different types, False if they have the same type.

Sorry for the delay: I was out of town. Using the Haskell98
implementation of typesafe MRef posted earlier, the insert2 function
always returns True. To be more precise, the following function,


insert2 val1 val2 =
  let
 (m1,k1) = insert empty () [val1]
 (m2,k2) = insert m1 () [val2]
 m3 = update m2 k1 []
  in
 isJust (lookp m3 k2)

re-written to conform to Simon Peyton-Jones' signature (modulo
renaming of lookup into lookp) and to use lists rather than
Maybes. The universe in the posted code had no maybes, due to my
laziness.

The function continues to always return True even if we replace the
update statement above with
 m3 = update m2 k2 []

The former result is obvious from the fact that keys k1 and k2 indeed
refer to different "cells" so to speak (at least in the posted
implementation of the Simon Peyton-Jones' signature). Therefore,
updating the cell referred to by k1 has no bearing on the cell
referred to by k2.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Overlapping instances in existentials

[oleg]

Ed Komp replied to Simon Peyton-Jones:
> Within the GHC compiler
>  > can't be instantiated to Double --- but that's tricky to pin down.
> this may be tricky to pin down.
> But, there is specific information in my example to exclude Double:
> I had carefully constructed the type definitions to avoid
> ambiguity.

Indeed, the open world assumption makes it rather difficult to define
a constraint that two type variables must denote different types. I
wish it were possible to easily write
forall a b. (NotEq a b) => ...

Functional dependencies can be used to achieve a similar effect -- but
sometimes that are not applicable. I wish there were a way to assert
to the compiler that there will be no more instances of a specific
class. The compiler can record this assumption in the object
file. When the compiler builds the final executable and finds an
unexpected instance, the compiler can tell the user that he lied.

 > | class SubType a b where
 > |   inj :: a -> b
 > |   prj :: b -> Maybe a
 > |
 > | instance SubType a (Either a x) where
 > |   inj   =3D Left
 > |   prj   =3D either Just (const Nothing)
 > |
 > | instance (SubType a b) =3D> SubType a (Either x b) where
 > | inj   =3D Right . inj
 > | prj   =3D either (const Nothing) prj
 > |
 > | type BaseType = Either Integer ( Either Bool () )
 > |
 > | type Value = (Either Double BaseType)
 > |
 > | data Foo =  forall x. (SubType x BaseType)  => MkFoo x
 > |
 > | test :: Foo -> Value
 > | test (MkFoo x) = inj x


I'm quite dubious that test can be typed at all (see below). Even if
the problem with overlapping instances could be solved. I seem to
remember being on this road before. I'd be great to get GHC to run the
typechecker at run time, to choose the right instance. Alas.

In the example above, the constraint on Foo only guarantees (SubType x
BaseType). When we create MkFoo True, for example, the compiler knows
the type the value being encapsulated, chooses the right instance
(that is, the dictionary), and places the dictionary and the value
into the MkFoo envelope. The function test executes "inj x" whose
return type is different from the BaseType. that is, 'inj' implicitly
has the constraint (SubType x Value). However, MkFoo x only guarantees
(SubType x BaseType). This is not a technicality. Let us disambiguate
the instances and remove all overlapping:

> class SubType a b where
>inj :: a -> b
>prj :: b -> Maybe a

> instance SubType Bool (Either Bool x) where
>inj   = Left
>prj   = either Just (const Nothing)

> instance SubType Integer (Either Integer x) where
>inj   = Left
>prj   = either Just (const Nothing)

> instance (SubType Bool b) => SubType Bool (Either Integer b) where
>  inj   = Right . inj
>  prj   = either (const Nothing) prj

> instance (SubType Bool b) => SubType Bool (Either Double b) where
>  inj   = Right . inj
>  prj   = either (const Nothing) prj

> instance (SubType Integer b) => SubType Integer (Either Double b) where
>  inj   = Right . inj
>  prj   = either (const Nothing) prj

> type BaseType = Either Integer ( Either Bool () )

> type Value = (Either Double BaseType)

> data Foo =  forall x. (SubType x BaseType)  => MkFoo x

> -- test :: Foo -> Value
> -- test (MkFoo x) = inj x

> test1 :: Foo -> BaseType
> test1 (MkFoo x) = inj x

This code types and even runs:

*> test1 $ MkFoo True
*> Right (Left True)

Indeed, when the compiler sees MkFoo True, it chooses the right instance
of the class (SubType x BaseType), and packs the corresponding
dictionary into MkFoo. When we run test1 $ MkFoo True, the compiler
extracts the dictionary from MkFoo, extracts the field inj from that
dictionary, and runs the corresponding procedure. At this time (at run
time), the compiler does not and cannot choose instances.

If we uncomment the procedure test above, we predictably get the
error:

/tmp/k2.hs:32:
Could not deduce (SubType x Value)
from the context (SubType x BaseType)
Probable fix:
Add (SubType x Value)
to the existential context of a data constructor
Or add an instance declaration for (SubType x Value)
arising from use of `inj' at /tmp/k2.hs:32
In the definition of `test': inj x

As we saw above, we cannot widen the constraint at the run time. The
function test wants to use a different function inj -- not the one
associated with (SubType Bool BaseType) -- the chosen instance -- but
a different one, associated with an instance (SubType Bool
Value). However, we cannot chose the instance at that time because the
compiler does not know the exact type of the value in the existential
envelope. To do as you wish, the compiler would have had to compile the
typechhecer into the target executable code. Not that it would be a bad
idea.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Function composition and currying

[oleg]

What I nice application for a multi-variadic compositional operator
mcomp [1]. Only one operator does the trick, for functions of
arbitrary number of curried arguments. And I really mean the arbitrary
number of arguments, in both functions under composition. Given

> f1 x = x*x
> g2 a b = a + b
> g3 a b c = a + b + c

we can easily compose g2 with f1
*Main> (g2 `mcomp` f1) (1::Int) (2::Int)
9

and g3 with f1 
*Main> (g3 `mcomp` f1) (1::Int) (2::Int) (3::Int)
36

But we can just as easily compose f1 with g2:
*Main> (f1 `mcomp` g2) (2::Int) (3::Int)
7
(that is, square the first number and add the second)

and f1 with g3
*Main> (f1 `mcomp` g3) (2::Int) (3::Int) (4::Int)
11


What's more, we can even compose g2 with g3 or g3 with g2!

*Main> (g3 `mcomp` g2) (1::Int) (2::Int) (3::Int) (4::Int)
10
*Main> (g2 `mcomp` g3) (1::Int) (2::Int) (3::Int) (4::Int)
10

The Web page referenced below shows an advanced application of mcomp, to
point-free programming (categorical products).

[1] http://pobox.com/~oleg/ftp/Haskell/types.html
The following code, excerpted from [1], was used for the above
examples. -fglasgow-exts are needed.

> class MCompose f2 cp gresult result | f2 cp gresult -> result, f2->cp
>   where
> mcomp:: (f1->f2) -> (cp->gresult) -> (f1 -> result)
>   
> -- Class instances. Please keep in mind that cp must be a non-functional type
> -- and f2 and cp must be the same. These instances enumerate the base cases.
> 
> instance MCompose (Maybe b) (Maybe b) c c where
> --mcomp f::(a->(Maybe b)) g::((Maybe b)->c) :: a->c
> mcomp f g = g . f
> 
> instance MCompose [b] [b] c c where
> --mcomp f::(a->[b]) g::([b]->c) :: a->c
> mcomp f g = g . f
>   
> instance MCompose Int Int c c where
> --mcomp f::(a->Int) g::(Int->c) :: a->c
> mcomp f g = g . f
> 
> instance MCompose Char Char c c where
> --mcomp f::(a->Char) g::(Char->c) :: a->c
> mcomp f g = g . f
> 
> instance MCompose (a,b) (a,b) c c where
> mcomp f g  =  g . f
> 
> -- Induction case
> instance (MCompose f2 cp gresult result) => 
>   MCompose (f1->f2) cp gresult (f1->result) where
> mcomp f g = \a -> mcomp (f a) g
> 
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Pure functional TypeRep [Was: Existentials...]

[oleg]

This message shows how to map _types_ to integers at compile time --
and then extend this facility to run-time so it can be used with
existentially-quantified types. It is statically guaranteed that
different types receive different integer labels. Unlike TyCons of
Dynamics, our mapping does NOT rely on unsafePerformIO. We use the
typechecker itself to compare types. It seems our typemap can also be
used for _safe_ casts, in particular, for casting away the existential
blemish.

This message was inspired by Amr Sabry's problem on
existentials. Unlike Hal Daume's solution posted here earlier, we do
not use Dynamics nor GMap -- therefore, we completely avoid
unsafePerformIO and unsafeCoerce. Our solution is purely functional
and assuredly type-safe (to the extent the typechecker can be
trusted). Extensions used:
  -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances

First, the compile-time mapping from types to integers.

Polytypic list:

> data Nil t r  = Nil
> data Cons t r = Cons t r
>
> class PList ntype vtype cdrtype where
> cdr::   ntype vtype cdrtype -> cdrtype
> empty:: ntype vtype cdrtype -> Bool
> value:: ntype vtype cdrtype -> vtype
>
> instance PList Nil vtype cdrtype where
> empty = const True
>
> instance (PList n v r) => PList Cons v' (n v r) where
>  empty = const False
>  value (Cons v r) = v
>  cdr   (Cons v r) = r

and the finite map from types to integers

> class TypeSeq t s where
> type_index:: t -> s -> Int
>
> instance (PList Cons t r) => TypeSeq t (Cons t r) where
> type_index _ _ = 0
>
> instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where
> type_index v s = 1 + (type_index v $ cdr s)

Let us build some finite map

> init_typeseq = Cons (undefined::Char) $
>Cons (undefined::Int) $
>Cons (undefined::Bool) $
>Cons (undefined::String) $
>Cons (undefined::Maybe Char) $
>Nil

A typeseq maps a type to an integer -- which is the type's position in
the polytypic list. We are satisfied with the first occurrence of the
type in the list. It is plain that a typeseq maps different types to
different integers. Let us see how it works:

-- *Main> type_index True  init_typeseq
-- 2
-- *Main> type_index 'a'  init_typeseq
-- 0
-- *Main> type_index "a"  init_typeseq
-- 3
-- *Main> type_index (1::Int)  init_typeseq
-- 1
-- *Main> type_index (Just 'a')  init_typeseq
-- 4
-- *Main> type_index (Just True)  init_typeseq

-- :1:
-- No instance for (TypeSeq (Maybe Bool) (Nil t r))
-- arising from use of `type_index' at :1
-- In the definition of `it': type_index (Just True) init_typeseq

We call this mapping compile-time because the translation from a type
to the corresponding encoding (1+1+...1) is done at compile time, when
the appropriate instance of the TypeSeq class is chosen. A
sufficiently smart compiler can just as well fold the constant
expression (1+1...+1) down to a single integer. Also, errors in the
translation are reported at compile-time.

However, to apply the mapping to existential types, we need to extend
the former to run-time.

> class TypeRep t where
> tr_index:: t -> Int
>
> -- All of the following are almost the same.
> -- The Template Haskell can really help us here
> instance TypeRep Char where
> tr_index x = type_index x init_typeseq
>
> instance TypeRep Int where
> tr_index x = type_index x init_typeseq
>
> instance TypeRep Bool where
> tr_index x = type_index x init_typeseq
>
> instance TypeRep String where
> tr_index x = type_index x init_typeseq
>
> instance TypeRep (Maybe Char) where
> tr_index x = type_index x init_typeseq

Now, Amr Sabry's Problem

> data F a b = 
>   forall c. (TypeRep c) => PushF (a -> c) (F c b) 
> | Bottom (a -> b)
>
> f1 :: Char -> Bool
> f1 'a' = True
> f1 _ = False
>
> f2 :: Bool -> String
> f2 True = "true"
> f2 False = "false"
>
> f3 :: String -> Int
> f3 = length
>
> fs = PushF f1 (PushF f2 (PushF f3 (Bottom id)))

First, we make fs an instance of class Show. It is jolly convenient.

> data HF = forall a b. (TypeRep a,TypeRep b) => HF (F a b)
> show_fn_type (g::(a->b)) 
>   = "(" ++ (show (tr_index (undefined::a))) ++ 
> "->"++(show (tr_index (undefined::b))) ++ ")"
>   
> instance (TypeRep a, TypeRep b) => Show (F a b) where
> show = show . hsf_to_lst . HF
>   where
>hsf_to_lst (HF (Bottom g)) = [show_fn_type g]
>hsf_to_lst (HF (PushF g next)) = (show_fn_type g):(hsf_to_lst$HF next)

Now, Amr Sabry's question:

] Is it possible to write a function 
]   f :: F a b -> T c -> F c b
] where (T c) is some type for values of type 'c' or values representing
] the type 'c' or whatever is appropriate. Thus if given the
] representation of Bool, the function should return:
]  PushF f2 (PushF f3 (Bottom id))
] and if given the representation of String the function should return
]  PushF f3 (

*safe* coerce, for regular and existential types

[oleg]

This message describes functions safeCast and sAFECoerce implemented
in Haskell98 with common, pure extensions. The functions can be used
to 'escape' from or to existential quantification and to make
existentially-quantified datatypes far easier to deal with. Unlike
Dynamic, the present approach is pure, avoids unsafeCoerce and
unsafePerformIO, and permits arbitrary multiple user-defined typeheaps
(finite maps from types to integers and values).

An earlier message [1] introduced finite type maps for
purely-functional conversion of monomorphic types to unique
integers. The solution specifically did not rely on Dynamic and
therefore is free from unsafePerformIO. This message shows that the
type maps can be used for a safe cast, in particular, for laundering
existential types. The code in this message does NOT use
unsafePerformIO or unsafeCoerce. To implement safe casts, we define a
function sAFECoerce -- which works just like its impure
counterpart. However the former is pure and safe. sAFECoerce is a
library function expressed in Haskell with common extension. The
safety of sAFECoerce is guaranteed by the typechecker itself.

This whole message is self-contained, and can be loaded as it is in
GHCi, given the flags
  -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances

This message was inspired by Amr Sabry's problem on existentials.  In
fact, it answers an unstated question in Amr Sabry's original message.


It has been observed on this list that existentially-quantified
datatypes are not easy to deal with [2]. For example, suppose we have
a value of a type

> data EV = forall a. (TypeRep a TI)=> EV a

(please disregard the second argument of TypeRep for a moment).

The constructor EV wraps a value. Suppose we can guess that the
wrapped value is actually a boolean. Even if our guess is correct, we
*cannot* pass that value to any function of booleans:

*> *Main> case (EV False) of (EV x) -> not x
*>
*> :1:
*> Inferred type is less polymorphic than expected
*> Quantified type variable `a' is unified with `Bool'
*> When checking an existential match that binds
*> x :: a
*> and whose type is EV -> Bool
*> In a case alternative: (EV x) -> not x

A quantified type variable cannot be unified with any regular type --
or with another quantified type variable. Values of existentially
quantified types cannot be passed to monomorphic functions, or to
constrained polymorphic functions (unless all their constrains have
been mentioned in the declaration of the existential). That limitation
guarantees safety -- on the other hand, it significantly limits the
convenience of existential datatypes [2].

To overcome the limitation, it _seemed_ that we had to sacrifice
purity. If we are positive that a particular existentially quantified
value has a specific type (e.g., Bool), we can use unsafeCoerce to
cast the value into the type Bool [3]. This approach is one of the
foundations of the Dynamic library. The other foundation is an ability
to represent a type as a unique run-time value, provided by the
methods of the class like TypeRep. Given an existentially quantified
value and a value of the desired type, Dynamic compares type
representations of the two values. If they are the same, we can
confidently use unsafeCoerce to cast the former into the type of the
latter.

This works, yet leaves the feeling of dissatisfaction. For one thing,
we had to resort to an impure feature. More importantly, we placed our
trust in something like TypeRep and its members, that they give an
accurate and unique representation of types. But what if they lie to
us, due to a subtle bug in their implementation? What if they give the
same representation for two different types? unsafeCoerce will do its
dirty work nevertheless. Using the result would lead to grave
consequences, however.

This message describes sAFECoerce and the corresponding safe cast.
Both functions convert the values of one type into the target type.
One or both of these types may be existentially quantified.  When the
source and the target types are the same, both functions act as the
identity function. The safe cast checks that the type representations
of the source and the target types are the same. If they are, it
invokes sAFECoerce. Otherwise, we monadically fail. The function
sAFECoerce does the conversion without any type checking. It always
returns the value of the target type. If the source type was the same
as the target type, the return value has the same "bit pattern" as the
argument. If the types differ, the return value is just some default
value of the right type. The user can specify the default value as he
wishes.

Therefore, we can now write

*> *Main> case (EV False) of (EV x) -> not $ sAFECoerce x
*> True

We can also try

*> *Main> case (EV 'a') of (EV x) -> not $ sAFECoerce x
*> *** Exception: Prelude.undefined

The default value was 'undefined'.

The function safeCast is actually trivial

> safeCas

*safe* coerce: four methods compared

[oleg]

This is a "Related Work" section of the previous message. We compare
three main methods of achieving safe casts. It seems that the method
proposed in the earlier message is quite different -- especially in
terms of extensibility. In this message, we compare the extensibility
of four techniques. Stephanie Weirich ICFP'00 paper points out another
solution, which relies on mutable IORefs. Since that technique can
only be used with IO monad, we do not consider it here.

Some of the methods below require type classes and algebraic datatype
declarations. Some require only an algebraic datatype, or only a
typeclass. In either case, we run into an extensibility problem: to
add support for a new datatype, we must either add an instance
declaration, or a new alternative to the datatype declaration. These
are non-trivial, non-modular extensions. For example, when we add a
new alternative to a datatype declaration, we must physically update
the corresponding file. We must then re-compile all dependent modules.

Surprisingly, the solution in the earlier message is free from these
drawbacks. We can extend the type heap in a modular fashion. We do not
need to alter type or data declarations. It seems our type heaps are
sort of reified lists of instances. There appear to be a duality
between typeclasses and our type heaps. Only our type heaps are
first-class.


The idea behind all type-safe casts is simple: to cast a value of a type
'a' into a target type 'b', we inject the value into some universe and
then project it to the target type 'b'.

To illustrate the differences in implementations of that idea, we will
be using James Cheney and Ralf Hinze's example: a generic comparison
function. To avoid unnecessary complications, we limit ourselves to
built-in and scalar types. Extensions to products, exponential,
recursive and polymorphic types are possible, but too messy. We also
will not consider existential types, so we avoid introducing type
classes if they are not needed in the static case.

This whole message is self-contained, and can be loaded as it is in
GHCi, given the flags
  -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances


Approach 1: Tcl approach

The universal type is a string. The values to cast must belong to the
class Show and the class Read. The injection and projection functions
are trivial:

> sh_inj x = show x
> sh_prj x = read x

Generic equality and the cast functions are trivial as well:

> sh_gequal x y = sh_inj x == sh_inj y

> sh_cast x = sh_prj $ sh_inj x

Here's the test:

> sh_test1 = [sh_gequal 1 2, sh_gequal True True, sh_gequal 'a' 'b']

To add support for a new datatype, we have to place that datatype in
the class Show and the class Read. That is, we have to add the
corresponding instance declarations _and_ we have to implement methods
'show' and 'read'. Functions sh_gequal and sh_cast do not have to be
modified. The Tcl approach is also the most generous with respect to
type equivalence: for example, Int and Integer are considered
equivalent, and sh_cast may cast between them.

Incidentally, when GHC can derive Binary, this approach becomes far
more appealing.


Approach 2: The universe is the tagged union

> data TU = TChar Char | TBool Bool | TInt Int
>
> class TURepr t where
>   tu_inj:: t -> TU
>   tu_prj:: TU -> t
> 
> instance TURepr Char where
>   tu_inj = TChar
>   tu_prj (TChar x) = x
>  
> instance TURepr Bool where
>   tu_inj = TBool
>   tu_prj (TBool x) = x
> 
> instance TURepr Int where
>   tu_inj = TInt
>   tu_prj (TInt x) = x
> 
> tu_gequal x y = cmp (tu_inj x) (tu_inj y)
>   where
> cmp (TChar x) (TChar y) = x == y   
> cmp (TBool x) (TBool y) = x == y   
> cmp (TInt x)  (TInt y)  = x == y   
>
> tu_cast x = tu_prj $ tu_inj x
>
> tu_test1 = [tu_gequal (1::Int) (2::Int), tu_gequal True True, 
> tu_gequal 'a' 'b']


To add support for a new datatype, we have to add a new alternative to
the declaration of the datatype TU and we have to add a new instance
for the class TURepr (with the implementation of the tu_inj and
tu_proj methods). We also have to add another clause to the tu_gequal
function. Clearly this is the least extensible approach.


Approach 3: by Cheney and Ralf Hinze's
The universe is a set of inject/project pairs

> data IPP a =  IPPInt  (a->Int)  (Int->a) 
> | IPPChar (a->Char) (Char->a)
> | IPPBool (a->Bool) (Bool->a)
>   
> ipp_gequal (IPPInt  prj inj) x y = prj x == prj y
> ipp_gequal (IPPChar prj inj) x y = prj x == prj y
> ipp_gequal (IPPBool prj inj) x y = prj x == prj y
>
> ipp_cast (IPPInt xprj xinj) x (IPPInt yprj yinj) = yinj $ xprj x
> -- more should follow...
>
> ipp_test1 = [ipp_gequal (IPPInt  id id) (1::Int) (2::Int),
>  ipp_gequal (IPPBool id id) True True,
>  ipp_gequal (IPPChar id id) 'a' 'b']

To add a new primitive datatype, we should modify the declaration of
the datatype IPP and add a new alternative. We also need to add
cl

Re: *safe* coerce, for regular and existential types

[oleg]

> Does this technique extend to polymophic types?
Yes, of course. The type F a b in the earlier message was polymorphic.

> Let's say we have the following type:

> > data D a = C | D a

> Is it possible to index the type D a?

I have just lifted the polymorphic Maybe -- which is isomorphic to
your type. 
ti maybe_decon (Just True)
ti maybe_decon (Just 'a')
give different results. (ti maybe_decon Nothing) can give either the
same or different indices for different concrete types of
Nothing. It's all up to you. For each new datatype, the user has to
provide two functions: one to deconstruct the datatype into a
polymorphic array of values of already indexable types, and the other
is to re-construct the datatype from the array. As long as the user
can do that -- in _any_ way he wishes -- the mapping is
established. Incidentally, there is no need to add any new type
instances or add new alternatives to datatype declarations. There is
no need to extend the type heap either.

I could post the code but I need to write explanations and perhaps
change a few identifier names to something more meaningful. Alas, it's
already almost 2am, and I want to go home...
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: *safe* coerce: four methods compared

[oleg]

This message illustrates how safe casting with multiple universes can
be extended to new user-defined, polymorphic datatypes. We show a
_portable_ mapping of polymorphic types to integers. Different
instances of a polymorphic type map to different integers. Phantom
types can be either disregarded or accounted for -- as the user
wishes. Furthermore, if two different applications running on two
different machines agree on the same type heap, then they agree on the
type encoding. An application can use multiple typeheaps at the same
time. It is easy therefore to dedicate one particular typeheap for
portable encoding of types across several computers.

Incidentally, our encoding of types may take into account _values_ of
some of the components of a polymorphic type. For example, given a
value of a type 'Foo Int a', the encoding may use the _value_ of the
first component and the _type_ of the second component. When we do the
cast, we can check not only for the desired type but also for the
desired values. We can thus approach dependent types.

This message hopefully replies to Ralf Laemmel's comment:
] You should make very clear that there is
] not just a single safeCoerce, but the TI/init_typeseq argument has to
] be constructed and supplied by the programmer in a way that (s)he
] decides what array of types can be handled.  So if you wanted to use
] your approach to scrap boilerplate [1], say deal with many datatypes,
] this becomes quite a burden.  Think of actually building initial type
] sequences. Think of how combinators need to be parameterised to take
] type sequences.

with which I agree. Below I try to make it very implicit what depends
on TI/init_typeseq and what doesn't, and how much work is involved in
adding new datatypes and extending type heaps. I don't know if the
proposed approach is better than the others in many
circumstances. It's certainly different.

Ralf Laemmel also wrote:
] Software-engineering-wise your approach suffers from an important
] weakness: a closed world assumption.  The programmer has to maintain
] your "TI" and pass it on in all kinds of contexts for the array of
] types to be handled.

I thought it is a feature. I thought a programmer can import some type
heap, partially apply the needed function to it, and re-export the
latter. The example below demonstrates what is involved when a new
datatype is added. It seems not that much. 


] I didn't need undecidable not even overlapping instances.

I don't actually need overlapping-instances extensions. An earlier
message on the subject of MRefs used similar type heaps without any
need for -fallow-overlapping-instances. However I had to use numeral
types such as Succ (Succ ... Zero) rather than Int for type
indices. The current approach looks more elegant. Besides, you seem to
in favor of giving overlapping instances more acceptance, support and
legitimacy.

] Is it obvious to see that fetching stuff from the type sequences would
] be indeed efficient for long PLists?

The sequence of 'cdr' operations needed for fetching stuff is known
statically. A compiler might therefore do something intelligent.


This whole message is self-contained, and can be loaded as it is in
GHCi, given the flags
  -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances

We start with the boilerplate, which has changed a little (for
example, the class PLists now has a member function pllen).

> data Nil t r  = Nil
> data Cons t r = Cons t r
>
> class PList ntype vtype cdrtype where
> cdr::   ntype vtype cdrtype -> cdrtype
> empty:: ntype vtype cdrtype -> Bool
> value:: ntype vtype cdrtype -> vtype
> pllen:: ntype vtype cdrtype -> Int
>   
> instance PList Nil vtype cdrtype where
> empty = const True
> pllen = const 0
>   
> instance (PList n v r) => PList Cons v' (n v r) where
>  empty = const False
>  value (Cons v r) = v
>  cdr   (Cons v r) = r
>  pllen (Cons v r) = 1 + pllen r
> 
> class TypeSeq t s where
> type_index:: t -> s -> Int
> fetch:: t -> s -> t
> alter:: t -> s -> s
>   
> instance (PList Cons t r) => TypeSeq t (Cons t r) where
> type_index _ _ = 0
> fetch _ (Cons v _) = v
> alter newv (Cons v r)  = Cons newv r
>
> instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where
> type_index v s = 1 + (type_index v $ cdr s)
> fetch v s = fetch v $ cdr s
> alter newv (Cons v' r') = Cons v' $ alter newv r'

The initial typesequence:

> init_typeseq = Cons (undefined::Char) $
>Cons (undefined::Int) $
>  Cons (undefined::Bool) $
>  Cons (undefined::String) $
>  (Nil::Nil () ())

and its type. See the previous message for more discussion of the
latter.

> type TI 
>   = (Cons
> Char
> (Cons Int (Cons Bool (Cons String (Nil () ())

Because we will be dealing with existential types, we need to extend
the compile-time indexing into run-time:

> class (TypeSeq t u) => Type

Re: Type class problem

[oleg]

> I defined type recursion and naturals as

> >newtype Mu f = In {unIn :: f (Mu f)}
> >data N f = S f | Z
> >type Nat = Mu N

> An application of Mu should be showable if the functor maps showable types
> to showable types, so the most natural way to define the instance seemed
> to be

> instance (Show a => Show (f a)) => Show (Mu f) where
>   show (In x) = show x

> Of course that constraint didn't work.

Well, it can if we write it in a bit different way:

instance (Show (f (Mu f))) => Show (Mu f) where
   show (In x) = show x

instance Show (N (Mu N)) where
   show Z = "Z"
   show (S k) = "S "++show k

*Main> show (In (S (In (S (In Z)
"S S Z"

This solution is akin to that of breaking the type recursion when
defining the fixpoint combinator fix. Only here we face the recursion
on constraints. I believe the same solution should work for the
Observable class. You didn't post the definition of the Observable
class, so I couldn't test my claim.

Flags used:
ghci -fglasgow-exts -fallow-undecidable-instances  /tmp/a.hs
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[oleg]

Wolfgang Jeltsch has observed:
> I have this code:
> class C a b c | a b -> c where
> f :: a -> b -> c
>
> instance C a b c => C a (x,y,b) c where
> f a (_,_,b) = f a b
>
> instance C a (a,c,b) c where
> f _ (_,c,_) = c
> ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
> complaint but hugs -98 +o says:
> ERROR "ClassProblem.hs":7 - Instances are not consistent with
> dependencies
> *** This instance: C a (a,b,c) b
> *** Conflicts with   : C a (b,c,d) e
> *** For class: C a b c
> *** Under dependency : a b -> c
> Can anyone tell me what the reason for this is and, maybe, how to avoid
> these problems with Hugs?

I believe it's helpful to think about this problem in terms of logical
programming, and proceed in phases.

Phase 1. The compiler sees the instances of a class C and compiles
them into a database of instances. In Prolog terms, given the
instances

instance C a b c => C a (x,y,b) c
instance C a (a,c,b) c

the compiler asserts

c(A,tuple(A,C,B),C,dict2).
c(A,tuple(X,Y,B),C,dict1) :- c(A,B,C,_).

In Haskell, lower-case type identifiers are variables and upper-case
one are type constants. In Prolog, it's the other way around:
lower-cased identifiers are constants and upper-cased are variables. I
hope that won't cause too much confusion.

I happen to have SWI-Prolog handy, in which I assert the above two
facts.

Phase 2. Suppose the compiler sees a type with a class constraint ``C Int
(Int,Char,Bool) t'' The compiler can determine the appropriate instance
by issuing a query:

?- bagof(Dict,c(int,tuple(int,char,bool),T,Dict),Dicts).

Dict = _G158
T = char
Dicts = [dict2] 
Yes

In our case, only one instance matched, and we found the corresponding
dictionary. If Dicts were a list of two or more dictionaries, we would
have needed to choose the most specific, if any.

Phase 1a.
Before we get to Phase 2 however, we have to take care of one more
problem. The class declaration specified a dependency:
class C a b c | a b -> c

which all members of that class must satisfy. The instances (which
define the membership) must be consistent with the dependency "a b -> c".
The consistency would be violated if there were two types "C a b c1"
and "C a b c2" such that c1 /== c2. Thus we can check the
consistency of the instances by searching for a counter-example:

?- c(A,B,C1,_), c(A,B,C2,_), \+ C1 == C2.

A = _G151
B = tuple(_G151, _G153, tuple(_G151, _G158, _G302))
C1 = _G153
C2 = _G158 
Yes

Alas, in this case we found a counter-example: types
C a (a,c,(a,c',d)) c
C a (a,c,(a,c',d)) c'

with c' /= c match some instance but contradict the functional
dependency. Therefore, the compiler complaints.



___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: container for different types, avoiding boiler plate

[oleg]

You might also wish to look at the typed heaps, which have been
discussed here on many occasions. Given the constant piece of code in
the appendix (which does *not* depend on user types and can be put
into a separate, constant module) you can write

> data Gender = Masc | Fem | Neutr   deriving (Show)
> data Number = First | Second | Third deriving (Show)
>
> attrs = Cons Masc $ Cons Second $ Nil
>
> ggender attrs = (fetch undefined attrs) :: Gender
> gnumber attrs = (fetch undefined attrs) :: Number

As you can see, functions ggender and gnumber are so trivial that
hardly need to be declared at all. You can just use fetch
directly. There is no need for Maybe. In fact, if you attempt to fetch
a type that you didn't put into the attrs, you get a _compile-time_
error.

*Main> ggender attrs
Masc
*Main> gnumber attrs
Second

Updates are allowed as well:

*Main> let attrs' = alter Neutr attrs in (ggender attrs', gnumber attrs')
(Neutr,Second)


Appendix: the constant part of the code.
Flags used:
-fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances

> data Nil t r  = Nil
> data Cons t r = Cons t r
>
> class PList ntype vtype cdrtype where
> cdr::   ntype vtype cdrtype -> cdrtype
> empty:: ntype vtype cdrtype -> Bool
> value:: ntype vtype cdrtype -> vtype
>   
> instance PList Nil vtype cdrtype where
> empty = const True
>
> instance (PList n v r) => PList Cons v' (n v r) where
>  empty = const False
>  value (Cons v r) = v
>  cdr   (Cons v r) = r
>
> class TypeSeq t s where
> type_index:: t -> s -> Int
> fetch:: t -> s -> t
> alter:: t -> s -> s
>   
> instance (PList Cons t r) => TypeSeq t (Cons t r) where
> type_index _ _ = 0
> fetch _ (Cons v _) = v
> alter newv (Cons v r)  = Cons newv r
>   
> instance (PList Cons t' r', TypeSeq t r') => TypeSeq t (Cons t' r') where
> type_index v s = 1 + (type_index v $ cdr s)
> fetch v s = fetch v $ cdr s
> alter newv (Cons v' r') = Cons v' $ alter newv r'
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

AW: container for different types, avoiding boiler plate

[oleg]

> > There is no need for Maybe. In fact, if you attempt to fetch
> > a type that you didn't put into the attrs, you get a _compile-time_
> > error.

> But I'm not sure if it's suitable for what I'm doing, as the attributes
> get inserted at run time, and not all of them appear everywhere. So
> Maybe is quite natural here.

The question then becomes: are the types of all attributes that might
appear in the list attrs are known at the compile time? If so, the
previous solution applies as it is, still retaining the static type
guarantees: unlike the solution involving Dynamics, an attempt
to fetch a value of the type not present among the "attributable"
types is a type error.

Using the constant code in the Appendix of the previous message, we
can write

> data Gender = Masc | Fem | Neutr   deriving (Show)
> data Number = First | Second | Third deriving (Show)
> data Color = Color {redval, greenval, blueval:: Int} deriving Show

Define all types that may appear in attributes. An attempt to place or
fetch some other type from init_attrs (or its altered variant) will be
a compile-time error.

> init_attrs = Cons (Nothing::Maybe Gender) $ 
>  Cons (Nothing::Maybe Number) $
>  Cons (Nothing::Maybe Color)  $ 
>  Nil

First we insert the values of some attributes at the run time (in the
let expression), and then retrieve them. We can insert and retrieve
the values in any order we wish. We can even delete values by
inserting Nothing cast to appropriate type.

> test :: (Maybe Color, Maybe Number, Maybe Gender) =
>   let attrs = alter (Just Masc) $
>   alter (Just (Color 0 0 255)) $
>   init_attrs
>   in (fetch undefined attrs, fetch undefined attrs,
>   fetch undefined attrs)


*Main> test
(Just (Color {redval = 0, greenval = 0, blueval = 255}),Nothing,Just Masc)

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Type class problem

[oleg]

Simon Peyton-Jones wrote:

> > instance (Show (f (Mu f))) => Show (Mu f) where
> >show (In x) = show x
> >
> > instance Show (N (Mu N)) where
> >show Z = "Z"
> >show (S k) = "S "++show k

> But again, it's fragile isn't it? You are dicing with non-termination
> if you have instance declarations where the stuff before the '=>' is more
> complicated than the stuff after the '=>'.  A less carefully written
> instance for Show (N (Mu N)) would make the type checker loop.

That's true that care is required. However, the same care is required
when we want to write 'fix' or a set of mutually recursive type
aliases. We have to introduce a real constructor somewhere to break
the loop. I'm curious if you could post an example of

> You are dicing with non-termination
> if you have instance declarations where the stuff before the '=>' is more
> complicated than the stuff after the '=>'. 

I'm wondering if the general method of avoiding non-termination can be
made to work in these more complex cases.

Incidentally, the constraint solver stack overflow problem can be
turned to our advantage. The typechecker's exhausting the stack should
be considered a failure to match the instance -- and so the
typechecker should mark the current instance inappropriate and try
another one, if any. I have just implemented this strategy in a logic
programming system I'm working on, and it works beautifully. I can
find counter-examples of Haskell instances violating functional
dependencies no matter in which order the instances are given.

Thank you!
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: proving the monad laws

[oleg]

Steffen Mazanek posed a problem: given the monad:

> data Error a = Error String | Ok a
> data TI a = TI (Subst -> Int -> Error (Subst, Int, a))
> instance Monad TI where
>  return x   = TI (\s n -> Ok (s,n,x))
>  TI f >>= g = TI (\s n -> case f s n of
>Ok (s',m,x) -> let TI gx = g x in
>   gx s' m
>Error s->Error s)
>  fail s = TI (\_ _->Error s)

prove the associativity of bind:

> m@(TI mf) >>= (\a->f a >>= h) =
>  = TI (\s n -> case mf s n of
>   Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in
>gx s' m
>   Error s->Error s)  =  ...
>  = ((TI mf) >>= f) >>= h
> I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in 
> ...".
> But the "a" may occur in "h"?

No, it may not. First of all, the third monadic law  specifically
disclaims such an occurrence. Indeed, if 'a' had occurred free in 'h', 
then ((TI mf) >>= f) >>= h would make no sense. 

Although (>>=) notation is better for practical programming, I
believe Filinski's notation is superior for manipulation. Filinski
defines a postfix operator "raised star", which is denoted 'st' below:

st:: (Monad m) => (a -> m b) -> m a -> m b
st f m = m >>= f

Indeed, st = flip (>>=)

In Filinski's notation, the third monadic law has an especially
appealing form:
st ((st f) . g) = (st f) . (st g)

Let us also define 
arun (TI f) s n = f s n

We can then write for our monad:

st f = \m -> TI $ \s n -> case arun m s n of
 Ok (s',m',x') -> arun (f x') s' m'
 Error s' -> Error s'

Let _m, _s and _n denote "fresh" values of the right type (so we can later
appeal to the universal generalization rule (closely related to eta-reduction)

Phase 1:

arun ((st ((st f) . g)) _m) _s _n
=>
case arun _m _s _n of
  Ok (s',m',x') -> arun ((st f) $ g x') s' m'  -- x' is not free in f, g
  Error s' -> Error s'
=>
case arun _m _s _n of
  Ok (s',m',x') -> case arun (g x') s' m' of
  Ok (s'',m'',x'') -> arun (f x'') s'' m''
  Error s'' -> Error s''
  Error s' -> Error s'


Phase 2:

arun (((st f) . (st g)) _m) _s _n
=>
arun (((st f) $ (st g) _m) _s _n
=>
case arun ((st g) _m) _s _n of
  Ok (s'',m'',x'') -> arun (f x'') s'' m''  -- x'' is not free in f, g
  Error s'' -> Error s''
=>
case (case arun _m _s _n of
  Ok (s',m',x') -> arun (g x') s' m'-- x' is not free in f, g
  Error s' -> Error s') of
  Ok (s'',m'',x'') -> arun (f x'') s'' m''  -- x'' is not free in f, g
  Error s'' -> Error s''
=> {see note below}
case arun _m _s _n of
  Ok (s',m',x') -> case arun (g x') s' m' of
   Ok (s'',m'',x'') -> arun (f x'') s'' m''
   Error s'' -> Error s''
  Error s' -> Error s'

Now, the results of Phase 1 and Phase 2 are identical.  Given that _m,
_s and _n were unique, fresh variables, by appealing to the universal
generalization rule and the Church-Rosser property of our reductions,
we conclude that

st ((st f) . g) = (st f) . (st g)

The critical step is the associativity of case:

  case (case x of C1 -> O1; C2 -> O2) of C1' -> O1'; C2' -> O2'
==>
  case x of 
 C1 -> case O1 of C1' -> O1'; C2' -> O2'
 C2 -> case O2 of C1' -> O1'; C2' -> O2'

provided that variables bound in C1 and C2 do not occur in C1', O1', C2', O2'
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: proving the monad laws

[oleg]

Hello!

> Would it be possible to write a piece of Haskell code which checks
> the monadic laws automatically by simulating evaluation in this way?

To some extent, yes. The proof in the previous message was based on
normalization, with respect to associative laws and some betas. So we
can take
(st f) . (st g)
and do:
- inlining of the 'st' operation
- de-sugaring into core Haskell
- more inlining and beta [perhaps to a certain depth]
- rearranging expression based on associative laws,
e.g., converting f . (g . h) into (f . g) . h
converting
   case (case x of P -> A) of P' -> A'
into
   case x of P -> case A of P' -> A'

Then do the same for (st ((st f) . g)) and compare the results. If the
results are identical, great. Otherwise, the user has to look at the
results and decide if they are the same based on his intuition.

GHC already does inlining, de-sugaring, and some betas. I think there
is a flag that makes GHC dump the result of these operations for
normalization with respect associative laws. BTW, GHC accepts
user-defined rules: so we can express associativity rules for known
operations and direct GHC to normalize terms with respect to these
laws. I don't know how to express side conditions though (e.g., the
normalization of 'case' above is valid only if the variables bound by
pattern P do not occur in P', A'). It would be great if there was a
RULES-pragma operation to alpha-rename bound variables in a term. In
that case, we can safely normalize more expressions.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Circular Instance declarations

[oleg]

Ashley Yakeley wrote:

> Would it be reasonable for the compiler to check back through the
> stack and allow the circularity? It will just create an ordinary
> recursive function.

The following works.

Flags: -fglasgow-exts -fallow-undecidable-instances

data D r = ZeroD | SuccD (r (D r))

instance (Eq (r (D r))) => Eq (D r) where
   ZeroD == ZeroD = True
   (SuccD a) == (SuccD b) = a == b
   _ == _ = False


newtype C a = MkC a

instance Eq (C (D C)) where
   (MkC ZeroD) == (MkC ZeroD) = True
   (MkC (SuccD a)) == (MkC (SuccD b)) = a == b
   _ == _ = False

equalDC :: D C -> D C -> Bool
equalDC = (==)

c2 = SuccD (MkC (SuccD (MkC ZeroD)))
c1 = SuccD (MkC (ZeroD))

*Main> equalDC c2 c2
True
*Main> equalDC c2 c1
False
*Main> equalDC ZeroD c1
False
*Main> equalDC ZeroD ZeroD
True
*Main>
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Polymorphic Recursion / Rank-2 Confusion

[oleg]

Dominic Steinitz wrote:
> My motivation in using this type was to see if, for example, I could
> restrict addition of a vector to another vector to vectors of the same
> length. This would be helpful in the crypto library where I end up having to
> either define new length Words all the time or using lists and losing the
> capability of ensuring I am manipulating lists of the same length.

Perhaps you might find the following

http://pobox.com/~oleg/ftp/Haskell/number-parameterized-types.html

relevant to your task. The page demonstrates bitvectors of a
statically-checked width. An attempt to AND or OR two bitvectors
of different widths results in a type error. The width can be
specified in _decimal_ rather than in binary, which makes types
smaller and far easier to read. Type error messages also become more
comprehensible. To implement just the width-checking, we need only
Haskell 98.

Incidentally, the approach can be easily extended to arbitrary bases,
e.g., base64. Therefore, we can define numerals over a field Z^{*}_p
whose modulus p is statically known and statically checked. It would
be a type error to add or multiply two numerals with different
moduli. With base64-bigits, we need only 86 bigits for a 512-bit
modulus. Eighty-six terms make a type expression a bit long, but still
manageable; whereas binary types such as Zero and One would make
the approach unfeasible.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

From enumerators to cursors: turning the left fold inside out

[oleg]

andle.

*Main> test_read tf 5
 reading from handle. Got '0'
 reading from handle. Got '1'
 reading from handle. Got '2'
 reading from handle. Got '3'
 reading from handle. Got '4'
Have read: "43210"

The following tests the exhaustive iteration.
*Main> test_read tf 20
 reading from handle. Got '0'
 reading from handle. Got '1'
 reading from handle. Got '2'
 reading from handle. Got '3'
 reading from handle. Got '4'
 reading from handle. Got '5'
 reading from handle. Got '6'
 reading from handle. Got '7'
 reading from handle. Got '8'
 reading from handle. Got '9'
Have read: "9876543210"

Let us suppose that make_hfold_left' is the only way to access
files. Can we recover ordinary i/o streams from it? The answer is
yes. We can get the familiar open, getchar and eof functions
from the half-baked enumerator. Furthermore, the derivation of these
functions is *independent* of the precise nature of the enumerator. We
will never need (nor be given) access to the handle.

> data MyStream = MyNil (Maybe Char) | MyCons Char (IO MyStream)
>
> myopen:: FileName -> Title -> IO MyStream
>
> myopen filename title = do
>   hfold_left' <- make_hfold_left' filename title
>   let k fn (MyNil Nothing)  = return $ MyNil Nothing
>   k fn (MyNil (Just c)) 
> = return $ MyCons c (hfold_left' k fn (MyNil Nothing))
>   hfold_left' k (\_ c -> Right $ MyNil $ Just c) (MyNil Nothing)

> mygetchar:: MyStream -> IO (Char,MyStream)
> mygetchar (MyCons c k) = k >>= (return . ((,) c))
>
> myiseof::   MyStream -> Bool
> myiseof (MyNil Nothing) = True
> myiseof _ = False

We can now test reading from two streams with interleaving:

> test_interleave fname = do
>   stream1 <- myopen fname "stream1"
>   stream2 <- myopen fname "stream2"
>
>   putStrLn "\nReading 2 chars from one stream"
>   (c1,stream1) <- mygetchar stream1
>   (c2,stream1) <- mygetchar stream1
>   putStrLn $ "Read: " ++ (show [c1,c2])
>
>   putStrLn "\nReading 3 chars from the second stream"
>   (c1,stream2) <- mygetchar stream2
>   (c2,stream2) <- mygetchar stream2
>   (c3,stream2) <- mygetchar stream2
>   putStrLn $ "Read: " ++ (show [c1,c2,c3])
>  
>   putStrLn "\nReading again 2 chars from the first stream"
>   (c1,stream1) <- mygetchar stream1
>   (c2,stream1) <- mygetchar stream1
>   putStrLn $ "Read: " ++ (show [c1,c2])

*Main> test_interleave tf
 reading from stream1. Got '0'
 reading from stream2. Got '0'

Reading 2 chars from one stream
 reading from stream1. Got '1'
 reading from stream1. Got '2'
Read: "01"

Reading 3 chars from the second stream
 reading from stream2. Got '1'
 reading from stream2. Got '2'
 reading from stream2. Got '3'
Read: "012"

Reading again 2 chars from the first stream
 reading from stream1. Got '3'
 reading from stream1. Got '4'
Read: "23"

Note that we read ahead by exactly one character. If we want to detect
EOF, that is inevitable (we need to attempt reading if we want to
detect EOF).

We should point out the relationship between hfold_left, hfold_left' and
myopen: hfold_left is the fixpoint of hfold_left'. OTH, myopen
captures the continuation of hfold_left' in an IO action. This
relationship once again illustrates that call/cc and Y are indeed two
sides of the same coin [3].


[1] General ways to traverse collections
http://pobox.com/~oleg/ftp/Scheme/enumerators-callcc.html

[2] An argument against cursors
http://srfi.schemers.org/srfi-44/mail-archive/maillist.html

[3] Self-application as the fixpoint of call/cc
http://google.com/groups?selm=7eb8ac3e.0309182239.5a64b3b1%40posting.google.com

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: type class problem

[oleg]

Dean Herington wrote:
> Can someone explain why the following doesn't work?

> {-# OPTIONS -fglasgow-exts #-}

> class R r where
>   rId :: r -> String

> class (R r) => RT r t where
>   rtId :: r -> t -> String

> data RPair r1 r2 = RPair r1 r2

> instance (R r1, R r2) => R (RPair r1 r2) where
>   rId (RPair r1 r2) = "RPair " ++ rId r1 ++ " " ++ rId r2

> class TPair t t1 t2 where
>   prj :: t -> (t1,t2)
>   inj :: (t1,t2) -> t

> instance (RT r1 t1, RT r2 t2, TPair t t1 t2) => RT (RPair r1 r2) t where
>  rtId (RPair r1 r2) t = "RT (RPair " ++ rtId r1 t1 ++ " " ++ rtId r2 t2 ++")"
>where (t1,t2) = prj t

You need a functional dependency. For example:

class TPair t t1 t2 | t->t1 t2 where
  prj :: t -> (t1,t2)
  inj :: (t1,t2) -> t

with this definition, the typechecker is satisfied.

Without the dependency, the compiler assumes that there may be several
instances:
TPair t t1 t2
and
TPair t t1' t2'

You claimed that RT r1 t1 and RT r2 t2 holds. But you didn't promise
that RT r1 t1' and RT r2 t2' will also hold. In other words,
(RT r1 t1, RT r2 t2, TPair t t1 t2)
reads as
(exists t1 t2. RT r1 t1, RT r2 t2, TPair t t1 t2)
rather than
(forall t1 t2. RT r1 t1, RT r2 t2, TPair t t1 t2)
(which you need to guarantee that the definition of (t1,t2) = prj t
can be typechecked). Notice that forall is _inside_ of parentheses,
on the assumption side (the negative side). 

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Enum on Float/Double

[oleg]

> I found a case where I really need:
>   f :: Float -> Float
> where
>   f x is the least y such that x < y

This seems to be the problem of finding the unnormalized epsilon:
the smallest positive number one can meaningfully add to the given
number x. If that x is 1.0, we're talking about the epsilon.

There are several approaches:

- Consult the file /usr/include/float.h and find FLT_EPSILON and
DBL_EPSILON there. One can write a Haskell program that parses that
file, if one so wishes.

- apply the formula epsilon = base^(1-p)

- write a program everybody has written in good old Fortran days

> nextafter1:: Float -> Float
> nextafter1 0 = 0
> nextafter1 x | GHC.Float.isNaN x = x
> nextafter1 x | GHC.Float.isInfinite x = x
> nextafter1 x = try (abs x)
>   where try d = let d1 = d/2
>   in if x + d1 == x then improve d1 d else try d1
>   -- improve a b
>   -- we know that the number we seek is between a and b
>   -- try to see if there is a number in between that
>   -- still can be meaningfully added to x
>   improve a b = let middle = (a+b)/2
> in if middle == b || middle == a then x + b
>else if x + middle > x 
> then improve a middle else improve middle b
  
Standard caveat applies: some overly smart compilers arrange for the
whole iteration to be done with CPU registers, which often have extra
precision. Therefore, one might need to disable optimizations or play
other tricks to force storing/reloading the number to/from memory.

> test_delta:: Float -> Float -> Bool
> test_delta x y = y > x && (let x'=x+(0.9*(y-x)) in x'==y || x'==x)

*Main> test_delta (1.0::Float) (nextafter1 (1.0::Float))
True
*Main> test_delta (0.1::Float) (nextafter1 (0.1::Float))
True
*Main> test_delta (-42.3e20::Float) (nextafter1 (-42.3e20::Float))
True
*Main> (nextafter1 (-42.3e50::Float))
-Infinity

We can also deal with denormalized numbers:

*Main> GHC.Float.isDenormalized (12.0e-40::Float)
True
*Main> test_delta (12.0e-40::Float) (nextafter1 (12.0e-40::Float))
True

> On Tue, 21 Oct 2003, Lennart Augustsson wrote:
> > So this has been a while, but i think that decodeFloat,
> > incrementing the mantissa, encodeFloat might work.

But what if the mantissa is 0xff? We are at mercy of encodeFloat
doing the right thing.

Furthermore, this technique doesn't seem to work with denormalized numbers

*Main> GHC.Float.decodeFloat (1.0::Float)
(8388608,-23)
*Main> GHC.Float.decodeFloat (nextafter1 (1.0::Float))
(8388609,-23)
*Main> GHC.Float.decodeFloat (0.1::Float)
(13421773,-27)
*Main> GHC.Float.decodeFloat (nextafter1 (0.1::Float))
(13421774,-27)

So far, so good. However,

*Main> GHC.Float.decodeFloat (12.0e-40::Float)
(13701584,-153)
*Main> GHC.Float.decodeFloat (nextafter1 (12.0e-40::Float))
(13701600,-153)

Indeed,
*Main> GHC.Float.encodeFloat 13701584 (-153) == (12.0e-40::Float)
True
*Main> GHC.Float.encodeFloat 13701585 (-153) == (12.0e-40::Float)
True

so incrementing the mantissa by one doesn't actually work in all circumstances.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: lifting functions to tuples?

[oleg]

Abraham Egnor wrote:

> The classic way to write a lift function for tuples is, of course:

> liftTup f (a, b) = (f a, f b)

> which has a type of (a -> b) -> (a, a) -> (b, b).  I've been wondering if
> it would be possible to write a function that doesn't require the types in
> the tuple to be the same, just that the types in the second tuple are the
> result of applying the type transformation implied in the function to be
> lifted to the types in the first tuple.

Well, it is possible in Haskell. It works even in Hugs!

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}


class Funnable a b | a->b where
f:: a -> b

instance Funnable Bool Int where
f = fromEnum
instance Funnable Char Float where
f = fromRational . toRational . fromEnum
 
class LP a b c d where
liftf:: (a, b) -> (c, d)

instance (Funnable a c, Funnable b d) => LP a b c d where
liftf (a,b) = (f a, f b)

Main> liftf (True,'z')
(1,122.0)
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: lifting functions to tuples?

[oleg]

The problem:

liftTup f (a, b) = (f a, f b)

of the signature
liftTup:: ?? -> (a,b) -> (c,d)

Again, it is possible to write this in Haskell with common extensions

> {-# OPTIONS -fglasgow-exts #-}

> import Data.Dynamic
> import Data.Maybe

> liftp f (a,b) = ((fromJust . fromDynamic . f . toDyn) a,
>  (fromJust . fromDynamic . f . toDyn) b)

*Main> :t liftp
forall a2 a a3 a1.
(Typeable a, Typeable a1, Typeable a2, Typeable a3) =>
(Dynamic -> Dynamic) -> (a1, a3) -> (a, a2)


> f1 x | isJust (fromDynamic x::(Maybe Int)) 
> = let y = fromJust $ fromDynamic x in toDyn $ (toEnum (y + 1)::Char)
> f1 x | isJust (fromDynamic x::(Maybe Float))
> = let y::Float = fromJust $ fromDynamic x in toDyn $ (round(y + 1)::Int)
> f1 x = x

*Main> liftp f1 (65::Int,1.0::Float) :: (Char,Int)
('B',2)

> f2 x | isJust (fromDynamic x::(Maybe Bool)) 
> = let y = fromJust $ fromDynamic x 
>   in toDyn $ ((toEnum (if y then 42 else 65))::Char)
> f2 x | isJust (fromDynamic x::(Maybe ()))
> = let () = fromJust $ fromDynamic x in toDyn $ (2.5::Float)
> f2 x = x

*Main> liftp f2 (True,()) :: (Char,Float)
('*',2.5)
*Main> liftp f2 (False,()) :: (Char,Float)
('A',2.5)
*Main> liftp f2 (False,1::Int) :: (Char,Int)
('A',1)

As has been discussed on this list on many occasions, Dynamic (and the
accompanied safe coerce) can be implemented in Haskell98 plus
existentials and multi-parameter classes with functional dependencies.

As a matter of fact, translating (a,b) into (c,d) doesn' seem to be
much different than the generic mapping. I think Strafunsky can
express such a transformation trivially. Right?

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: getting the path to the executing program

[oleg]

Hal Daume wrote:
> is there a function, related to getProgName, which returns the (absolute)
> path to the current program?

> basically, i want to be able to read a file which i know will be in the
> same directory as the current program, but not necessarily in the same
> directory that we're running it from.

Actually, if you want to read a file located in the same directory
as the executable itself, you don't need the absolute path of the
executable. You merely need any path to the executable that is valid with
respect to the working directory at the start-up time.

Some four years ago I wrote a similar code that seems to work reliably
across HP/UX, Solaris, Linux, FreeBSD and various versions of Winxx
(from Windows98 onwards). The application has been deployed in more
than thousand copies and nobody has complained regarding the path.
The application reliably finds the name of a file from the
application's own directory no matter how the application was invoked:
from its own directory by name, from its own directory as "./appname",
from its own directory by the absolute or relative (../dir/appname)
name, or from some other directory by the absolute or relative name,
or by a symbolic link.

The only assumption is that neither forward nor backward slash can
appear in a file path. The latter assumption seems to always hold on
Winxx, which takes the forward slash as a path delimiter too. On
Unixen, the backward slash in file names seems to appear only on
hacked systems. So, the failure of the approach in that case should be
considered a feature.

The algorithm is simple: remove the last path-component from argv[0]
and append the local file name to the result (which may be an empty
string). A path component is a sequence of characters that does not
contain a path delimiter. Note that argv[0] may not end in a path
delimiter.

The algorithm requires argv[0] as it is given by the OS. Alas, neither
GHC nor Hugs seem to give us that. Therefore, I'm inclosing the Scheme
code that implements the algorithm. I do not have the guts to post the
original code (which was in Perl).

If I may suggest, a Haskell implementation may want to give a
programmer a way to obtain the unmangled argv0.


; last-delimiter STR -> POS
; where POS is the location of the last path-delimiter in STR
; or #f

(define delimiters '(#\\ #\/))

(define (last-delimiter str)
  (let loop ((i (- (string-length str) 1)))
(cond
  ((negative? i) #f)
  ((memv (string-ref str i) delimiters) i)
  (else (loop (- i 1))

(define local-file-name "that-is-it")

; Like with-input-from file, but the file
; is assumed to be in the same directory as the executable
; itself
(define (with-input-from-local-file local-file-name thunk)
  (let* ((argv0 (car (command-line)))
 (last-delim (last-delimiter argv0)))
(with-input-from-file
  (if last-delim
(if (< (+ 1 last-delim) (string-length argv0))
  (string-append (substring argv0 0 (+ 1 last-delim))
local-file-name)
  (error 'with-input-from-local-file
"path-delim at the end of argv0: " argv0))
local-file-name)
  thunk)))

(display (with-input-from-local-file local-file-name read))
(newline)

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

mfix as an effect

[oleg]

Can mfix be considered as "just a fix point combinator", without
any trace of effect?

The recent discussion about continuations and implementations of
Scheme in Haskell highlighted that question. The point of the
discussion is the difference between letrec implemented using the
fixpoint combinator, and a letrec implemented via an updateable cell
(as in Scheme, according to R5RS).

Ashley Yakeley wrote:

> > The difference between the Y and set! approaches to letrec *is*
> > observable.

> I don't believe you. My implementation uses Haskell's "mfix", which 
> looks like a Y to me. I certainly don't use anything like "set!".

That is, Ashley Yakeley claimed that his Haskell implementation of
Scheme implements letrec via Y -- and yet his implementation is
consistent with the R5RS semantics, which mandates the updateable-cell
letrec. Indeed, his implementation passes the tests designed to
discern the way letrec is implemented.

There seems to be a contradiction in the above statements. The
contradiction is resolved by noting that "mfix", although may look
like "Y", is fundamentally different. There is a latent "set!" in
mfix, which can be pried open with call/cc. There is an effect in
mfix. The following is a simple test that shows it.

Let us consider the following test (Scheme code first, Haskell code
follows).

(letrec
((fact
  (cons #f
(lambda (n)
  (set-car! fact #t)
  (if (zero? n) 1
  (* n ((cdr fact) (- n 1
  (let* ((before (car fact))
 (res ((cdr fact) 5)))
(list before res (car fact

The test has been introduced and discussed in
http://google.com/groups?selm=200102240312.TAA11588%40adric.cs.nps.navy.mil


If letrec is implemented via updates, the test returns (#f 120 #t)
If letrec is implemented via Y, the test should return (#f 120
#f). It is easy to see that if we use Y defined by (Y f) = f (Y f),
the result indeed must be (#f 120 #f).

Now, let us implement letrec in Haskell via fix and mfix, and compare
the results. First, the implementation of the test via fix

> import Data.IORef
> import System.IO.Unsafe
> import Control.Monad.Fix (mfix)

> fix f = f g where g = f g
> g = \f -> newIORef
>   (False, \n -> do
>   (flag,body) <- readIORef f
>   writeIORef f (True,body)
>   res <- if n ==0 then return 1 else
>  body (n-1) >>= return . (* n)
>   return res)
>
> g1 = \f -> unsafePerformIO (g f)
>
> test = let fact = fix g1 in do 
>  (flag,body) <- readIORef fact
>  res <- (body 5)
>  (flag',_) <- readIORef fact
>  return (flag, res,flag')


The code matches the Scheme code in every detail. If we try

> *Main> test >>= putStrLn . show
> (False,120,False)

we obtain the expected result. Now, we bring in mfix:

> test2 = do 
>  fact <- mfix g
>  (flag,body) <- readIORef fact
>  res <- (body 5)
>  (flag',_) <- readIORef fact
>  return (flag, res,flag')

And, quite predictably,

> *Main> test2 >>= putStrLn . show
> (False,120,True)


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

GHC, functional dependency, rank-2 type

[oleg]

There appears to be a problem with GHC's handling of multi-parameter
constraints with functional dependencies in the context of rank-2
types. The problem is not present in Hugs.

Let us first consider a simple example:

> module Test where
> class Foo a
>
> class Bar a
>
> data Obj = Obj
>
> instance Bar Obj
>
> instance (Bar a) => Foo a
>
> foo:: (Foo a) => a -> String
> foo _ = "works"
>
> runFoo:: (forall a. (Foo a) => a -> w) -> w
> runFoo f = f Obj

Here, the type of foo indicates

> Test> :t foo
> foo :: Foo a => a -> String

that foo can be applied to the value of any type so long as it is in
class Foo. The type of runFoo says that runFoo takes a function that
can process the value of every type of class Foo. The function foo
seems to be such a function. Therefore, "runFoo foo" should be
well-typed. And it is, and it works, both in Hugs (version November
2002) and in GHC 6.0.1 (which is the current version for FreeBSD).

However, if we make the classes Foo and Bar seemingly multi-parameter,
the trouble begins:

> class Foo a b | a->b
>
> class Bar a b | a->b
>
> data Obj = Obj
>
> instance Bar Obj Obj
>
> instance (Bar a b) => Foo a b
>
> foo:: (Foo a b) => a -> String
> foo _ = "works"
>
> runFoo:: (forall a b. (Foo a b) => a -> w) -> w
> runFoo f = f Obj

In Hugs:

> Test> :t foo   
> foo :: Foo a b => a -> String
> Test> runFoo foo
> "works"

As before, the function foo promises to handle the value of any type a
so long as "Foo a b" is satisfied (for any b -- although there can be
only one such b, due to the functional dependency). The function
runFoo takes any function that can handle the value of any type "a"
subject to the "Foo a b" constraint. So, "runFoo foo" should be
well-typed and should work. And it is, in Hugs.

GHC 6.01 is a different matter, unfortunately. An attempt to load the
above code in GHC succeeds, with flags:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

Furthermore, the types of foo and runFoo seem to be in perfect match.

> *Test> :t foo
> foo :: forall a b. (Foo a b) => a -> String
> *Test> :t runFoo
> runFoo :: forall w. (forall a b. (Foo a b) => a -> w) -> w

And yet,

*Test> runFoo foo

:1:
Could not deduce (Bar a b) from the context (Foo a b)
  arising from use of `foo' at :1
Probable fix:
Add (Bar a b) to the expected type of an expression
In the first argument of `runFoo', namely `foo'
In the definition of `it': it = runFoo foo

Why all of the sudden does GHC need the constraint Bar a b? The
function foo didn't ask for that... However, if we define foo and
runFoo as follows:

> foo:: (Foo a b) => a -> b -> String
> foo _ _ = "works"
>
> runFoo:: (forall a b. (Foo a b) => a -> b -> w) -> w
> runFoo f = f Obj Obj

then both GHC and Hugs are happy: "runFoo foo" says that it works in both.

What's more bizarre, even the following works:

> runFoo:: (forall a b. (Foo a b) => a -> b -> w) -> w
> runFoo f = f Obj undefined

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: GHC, functional dependency, rank-2 type

[oleg]

John Tromp wrote:
> >>instance (Bar a) => Foo a

> I have tried to write code myself like in the last line,
> stating that any instance of one class should also be
> an instance of another class. But Hugs would complain about
> it.

You're right. Hugs needs to be told that the code is in an extended
Haskell, with popular extensions. Therefore, Hugs has to invoked as
"hugs -98". It seems -98 flag cannot be changed once the Hugs is
running. Incidentally, the previously posted code included rank-2
types -- which are flagrantly not in Haskell98. Therefore, without -98
flag, Hugs will have a lot to complain about.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: Functional dependencies interfere with generalization

[oleg]

I'm sorry to open an old wound. I've just had an insight for
a clarification.

On Nov 26, 2003 Ken Shan wrote:

> Consider the following code, which uses type classes with functional
> dependencies:
>
> {-# OPTIONS -fglasgow-exts #-}
> module Foo where
> class R a b | a -> b where r :: a -> b
>
> -- 1
> rr :: (R a b1, R a b2) => a -> (b1, b2)
> rr a = (r a, r a)
>
> -- 2
> data RAB a = RAB (forall b. (R a b) => (a, b))
> mkRAB :: (R a b) => a -> b -> RAB a
> mkRAB a b = RAB (a, b)
>
> Neither 1 nor 2 passes the type-checker (GHC 6.0.1).  The error messages
> are similar:
> Inferred type is less polymorphic than expected
> Quantified type variable `b2' is unified with another
> quantified type variable
> When trying to generalise the type inferred for `rr'
> Signature type: forall a b1 b2.
> (R a b1, R a b2) =>
> a -> (b1, b2)
> Type to generalise: a -> (b1, b1)

> In both cases, the compiler is failing to make use of functional
> dependencies information that it has at its disposal.  Specifically,
> it seems to me that, if two type variables b1 and b2 have been unified
> due to functional dependencies, making two constraints in the context
> identical, then the inner constraint ("inner" with respect to the scope
> of quantified type variables) should be ignored.

Regarding the function rr, I'm afraid I'm compelled to side with the
typechecker. It appears that the typechecker does make use of the
functional dependencies to reject the code because the user has
specified too general a signature. Exactly the _same_ error occurs in
the following code

ab:: a -> Maybe a
ab = Just

rrr:: a -> (Maybe a, Maybe a1)
rrr a = (ab a, ab a)

Inferred type is less polymorphic than expected
Quantified type variable `a1' is unified with another
quantified type variable `a'
When trying to generalise the type inferred for `rrr'
Signature type: forall a a1. a -> (Maybe a, Maybe a1)
Type to generalise: a1 -> (Maybe a1, Maybe a1)
When checking the type signature for `rrr'
When generalising the type(s) for `rrr'

Error messages are identical.

Because ab is a function rather than a method, there trivially is a
functional dependency between the function's argument and its result.

Furthermore, exactly the same error occurs in

:: a -> b
 x = x

Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with
another quantified type variable `a'
When trying to generalise the type inferred for `'
Signature type: forall a b. a -> b
Type to generalise: b -> b
When checking the type signature for `'
When generalising the type(s) for `'


Regarding the original function rr, the best solution seems to be to
let the compiler figure out its type. It seems in these circumstances
the most general type exists -- and thus the compiler can figure it
out.

Now, regarding function mkRAB. It seems there is a simple solution:

data RAB a = RAB (forall b. (R a b) => (a, b))
mkRAB a = RAB (a, r a)

Indeed, the class R a b promised that there is a function 'r' such
that given a value of type 'a' can produce a value of type 'b'. So, we
can make use of such a function.

One can object: in a value of a type RAB (forall b. (R a b) => (a, b)),
the types of two components of a pair `(a, b)' must be related by the
relation R a b. The values can in principle be arbitrary. What if one
wishes to create a value RAB (x,z) such that the value z has the type of
(r x) but is not equal to (r x)? Well, there is an underhanded way to
help that.

class R a b | a -> b where 
   r ::  a -> b
   r1 :: a -> Integer -> b

that is, we define an additional method that takes an integer and
somehow makes the value of a type 'b'. We may imagine an Array(s) of all
possible values of type 'b' (specialized for those types 'b' for which
there are instances of the class R) and the method r1 merely uses its
second argument to select from that array. In any case, Goedel showed
that quite many pleasant and unpleasant things can be encoded in
integers. The first argument of r1 is merely a window dressing to
make the typechecker happy.

Thus we can define

mkRAB' a b = RAB (a, r1 a b)

To make the code more concrete, we introduce two instances

instance R Int Char where {r = toEnum; r1 _ = toEnum . fromInteger}
instance R Float (Maybe Float) where
r = Just
r1 _ 1 = Nothing
r1 _ n = Just (fromRational $ toRational (n-1) / (2^(128+1)))


In the second instances, we take advantage of the existence of an
injection from IEEE floating-point numbers to integers.

We can try evaluating "mkRAB 65", "mkRAB' 65 66", "mkRAB' (1.0::Float)
0", etc. -- and everything works.

Building RAB values is not enoug

Re: [Haskell] Per-type function namespaces (was: Data.Set whishes)

[oleg]

Hello!

> So, how can you come up with a type class which provides a polymorphic
> 'add' function, considering you don't even know how many parameters
> each data type's individual add function uses?

Very easily: every Haskell function takes only one
argument. Always. Ever.

> For example, say I'm writing the Data.Complex module; there's a
> function in that module "phase :: RealFloat a => Complex a -> a".  So,
> how do you put this phase function into a type class?  Perhaps you
> could abstract away from the RealFloat and Complex bits, so you have a
> phase function which is generalised to work over a Num and an
> arbitrary data type instead; e.g. "class Phase c where phase :: Num a
> => c a -> a".  But what happens if, say, somebody adds a Moon data
> type, and they want to write a phase function which returns the phase
> of such a moon?  Phases of the moon certainly aren't Nums, nevermind
> the fact that you probably want to supply your moon phase's function
> with some sort of date as an extra parameter, which means the Phase
> type class isn't flexible enough.

Here's the code that does exactly as you wish:

> {-# OPTIONS -fglasgow-exts #-}
>
> import qualified Complex 
>
> class Phase a b | a -> b where
>   phase:: a -> b
> 
>
> instance (RealFloat a) => Phase (Complex.Complex a) a where
> phase = Complex.phase
>   
> data MoonPhase = P1 | P2 | P3 | P4 deriving Show
>
> instance Phase Int MoonPhase where
> phase x = if x `mod` 4 == 0 then P1 else P4
>   
> instance Phase MoonPhase (Int->Int) where
> phase P1 x = x
> phase P2 x = x+1
>
> main = do
> putStrLn $ show $ phase ( (1.0::Float) Complex.:+ (1.0::Float))
> putStrLn $ show $ phase (0::Int)
> putStrLn $ show $ phase P1 (2::Int)

You can evaluate a phase of a complex number, get a phase of the moon
corresponding to some integer, and even convert a phase of the moon to
a time (given another integer as a reference time). Whereas the first
two functions take one argument, the latter phase takes "two
arguments". The class Phase takes the classical first-argument
overloading. Other overloading schemes are possible (e.g., the ones
that overload based on the result -- something that C++ just can't do:
e.g., Read). If we need to evaluate phases of Saturn moons (and we
overload on the first argument), we can resolve the overloading using
newtype:

> newtype SaturnTime a = ST a
> instance Phase (SaturnTime Int) (Int -> MoonPhase) where
>phase x moon_index = P1

newtypes add no run-time overhead, and actually help in making the
code more explicit.

Regarding Koening lookup: as I read in DDJ, it's just a hack! First
the committee added the namespaces, and then realized that using
operators like << became hugely inconvenient. So Koening came up with
a hack. Shouldn't a language be designed in a more systematic way?

Speaking of the language design, November 2003 issue of Dr.Dobbs
J. has an interesting article: "C++ Compilers and ISO Conformance" [by
Brian A. Malloy, James F. Power and Tanton H. Gibbs, pp. 54-60].

Here's a summary. C++ standard has been ratified by the ISO Committee
in September 1998. There is no conformance suite however. So, we
cannot tell how well a particular compiler complies with a
standard. The authors of an article decided to create an approximate
conformance suite -- from the examples given in the standard
itself. It's a hard job -- the examples aren't meant to be a compiled
code, so some declarations and other pieces have to be filled in. The
result cannot be considered a truly compliance suite because not all
features of the language are illustrated in examples, and the
distribution of the examples is uneven. Nevertheless, it's a start.

The authors of the article have tested several compilers. The bottom
line -- after five years, no single compiler fully complies with the
standard. The best compiler, from the Edison Group (a three-person
company) fails only 2 tests. Intel's compiler fails three. Visual C++
7.1 from Microsoft fails 12. Gcc 3.3 fails 26. The latter number shows
that a wide community participation and OpenSource do not necessarily
lead to a better product. Gcc 3.3 is also one of the slowest
compilers.

But there is worse news for C++. C++ Language Standard consists of 776
pages, describing C++ language and the C++ core library. At present,
411 points in the C++ language part and 402 points in the library
part have been identified as questionable or outright erroneous. 93
language issues have been already acknowledged as errors. That is,
EVERY page of the standard, on average, contains some issue! The
committee obviously didn't bother to check their examples. Well, even
now there isn't a compiler that complies with the standard -- whatever
the compliance may mean.

Not only programmers don't know what some C++
rules mean. Not only compiler writers are puzzled. Even the committee
itself obviously doesn't know how _many_ features are supposed to
work. Can you imagine more sh

[Haskell] Re: performance tuning Data.FiniteMap

[oleg]

Hello!

If indeed the read performance is at premium and updates are
infrequent, by bother with ternary etc. trees -- why not to use just a
single, one-level array. Given a reasonable hash function, the
retrieval performance is O(1). And still, no IO/ST are necessary.


{-# OPTIONS -fglasgow-exts #-}
module Foo where

import Data.Array
import Data.List

import Data.HashTable (hashString)
import Data.Int (Int32)

class Hashy a where
  hash:: a -> Int
  
data MyFM key val = MyFM { base::  Int
 , purgatory:: [(key,val)]
 , store:: Array Int [(key,val)]
 } deriving Show
 

empty = MyFM {base = 41, purgatory = [],
  store = listArray (0,base(empty)-1) $ repeat []}
  
lkup fm key = case lookup key (purgatory fm) of
 t@(Just _) -> t
 _  -> lookup key item
   where item  = (store fm)! hashv
 hashv = (hash key) `mod` (base fm)
 
count = length . concat . elems . store

purgatory_limit = 10

ins fm key val 
 = rebuild_perhaps $ fm {purgatory = add_uniq (purgatory fm) key val}
  where
   rebuild_perhaps fm | length (purgatory fm) > purgatory_limit 
  = rebuild fm
   rebuild_perhaps fm = fm
   
rebuild fm | 2*(count fm) > base fm = major_rebuild fm
rebuild fm = fm{purgatory = [], store = (store fm) // updates}
  where
updates = map (retr . merge) $ groupBy gfirs $ 
  sortBy sfirs $ map (\p@(k,v) -> (hashk k,p)) $ purgatory fm
hashk k = (hash k) `mod` (base fm)
gfirs (k1,_) (k2,_) = k1 == k2
sfirs (k1,_) (k2,_) = compare k1 k2
merge x = (fst$ head x, map snd x)
retr (h,v) = (h, unionBy gfirs v ((store fm)!h))

-- reallocate the hash table to the bigger size
major_rebuild fm = undefined -- exercise for the reader

-- add association (key,val) to the list, replacing an old association
-- with the same key, if any. At most one such association could have
-- existed
add_uniq [] key val = [(key,val)]
add_uniq ((hkey,_):t) key val | hkey == key = (key,val):t
add_uniq (h:t) key val = h: add_uniq t key val

instance Hashy String where
hash = fromInteger . toInteger . hashString



test1 = foldl (\fm v -> ins fm v v) empty $ map (:[]) ['a'..'h']
test2 = foldl (\fm v -> ins fm v v) test1 $ map (:[]) ['a'..'o']
test3 = foldl (\fm v -> ins fm v v) test2 $ map (:[]) ['a'..'o']
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: [Haskell] Per-type function namespaces (was: Data.Set whishes)

[oleg]

Simon Peyton-Jones wrote:

> In Haskell today, you can at least tell what value is bound to each
> identifier in the program, *without* first doing type checking. 

I'm afraid I'm confused. In the following code

> data Z
> data S a
>
> class Card c where c2int:: c -> Int
>
> instance Card Z where c2int _ = 0
> instance (Card c) => Card (S c) where c2int _ = 1 + c2int (undefined::c)
>
> foo = c2int (undefined::(S (S (S (S Z)

how can one tell the value of foo without first doing the
typechecking? Without typechecking, we can't use c2int and can't even
construct any meaningful value of class Card. For c2int, the type is
the ``value.'' Overlapping instances, polymorphic recursion -- all
seem to make the value determination even more uncertain.

Andre Pang wrote:

> 1) now I have to manually declare a class definition for every single 
> function, and I have to declare it in advance before any module defines 
> that function (most serious problem; see below),

> However, declaring the instance first requires declaring the type
> class itself, and that _is_ a problem, because that's exactly what I'm
> trying to work around.  Without 20/20 hindsight, you cannot say with
> certainty what type signatures a "generic" function (like 'phase' or
> even 'add') can support, because it's not a generic function,

But in the solution posted previously, for each ad hoc overloadable
function, the corresponding class *always* has the same
signature:

class HasAdd a b | a->b where add:: a->b

Therefore, we don't need clairvoyance to define an overloadable
function that way. If I need an overloadable function add, I can go
ahead and define the above class, and then add an instance. I can do
that without knowing all possible overloadable instances of add,
present or future. What if somebody else did the same in some other
module? If that somebody else followed the conventions, he would
introduce exactly the same class declaration. If GHC or its developers
could somehow be persuaded to overlook _exact_ duplicate class
declarations, then that part of the problem can be solved. The class
declaration itself could perhaps be generated by Template Haskell.

The discussed solution is quite related to some of the Records
proposals (which have been discussed here half a year ago). There too
we have the inconvenience of choosing unique names for field labels.

> data Person = Person {_pname:: String, _paddress:: String}
> data Computer = Computer {_cname::[String], _caddress:: Int}
>
> class HasName a b | a->b where name:: a->b
> class HasAddress a b | a->b where address:: a->b
>
> instance HasName Person String where name = _pname
> instance HasAddress Person String where address = _paddress
> instance HasName Computer [String] where name = _cname
>
> instance (HasName n r) => HasName (Maybe n) (Maybe r) where
> name = fmap name
>
> -- Alas, the following will break the dependency...
> --instance (Num a) => HasName a String where name = show
>
> -- But the following works: overlapping instances at work
> instance (HasAddress a b) => HasName a b where name = address
>
> instance HasAddress Int (Int->String) where address x y = show (x+y)
>
> newtype W a = W a   
> instance (Num a) => HasAddress (W a) String where address (W a) = show a
>
> test2 = let p = Person  "Anonymous"  "N/A"
> c = Computer ["FQDN","localhost"] 10
>   in "person named " ++ (name p) ++ " at a computer " ++ (head (name c))
>  ++ " and another " ++ (show$ name p1)
>where p1 = (Nothing::Maybe Person)

The first few lines of the code is boilerplate and could be
automatically generated. As you can see, we can even handle a limited
form of polymorphism, and even do a "hand off". For example, if some
thing doesn't have a name but has an address, we can use the address
as its name. Alas this ``backtracking'' isn't as general as we might
wish. At some point we have to introduce wrappers (like W a above) to
hand over the dispatch to another class. It's possible to do the
dispatch on a class, but it's a bit too painful. OTH, the wrappers
such as 'W' may be considered as an 'alternative view' of an object.
By wrapping an object, we can switch its behavior from the main one to
an alternative without any run-time penalty.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: performance tuning Data.FiniteMap

[oleg]

[BTW, should we move to Haskell-Cafe?]

> Because updates are not so infrequent that I want to pay the cost of
> replicating the entire array every update (or every ten!).  I'm
> willing to exchange *some* read time for faster update. Also, because
> small array copies may be sufficiently faster than tree traversals
> that I may pay very little extra for faster reads.
>
> FYI, my current code looks like this:

I'm afraid I'm somewhat confused. The hash-table related code makes
the copy of the whole array every purgatory-size times. Thus, given the
sequence of 'n' unique inserts (which don't trigger the
major_rebuild), at most 2*n/|purgatory| elements will be moved.

As I understand your code, in particular,

>   insert (ArrMap proto toBase ht) key elt = ArrMap proto toBase newHT
>  where newHT= insert' proto ht (toBase key) elt
>   insert' _ (HT x _) [] = HT x
>   insert' proto (HT Nothing y) key = insert' proto (HT (Just proto) y) key
>   insert' p (HT (Just ar) y) (k:ey) = \val -> HT (Just $ newArray val) y
>   where newArray val = ar//[(k,insert' p (ar!k) ey val)]

you make a copy of an array of the size |base| |key| times. _If_ the
tree is kept balanced and filled, then the sequence of n inserts will
copy (log n)/(log |base|)*|base| elements. For small n and large
|base|, that can be a lot. For example,

>   testMap=newMap (chr 0) (chr 255) id
>   main = do print $ lookup (insert testMap "abc" (Just "def")) "abc"

involves copying a 256-element array three times. Right? 

I guess we have come to the point where we really need to know the
distribution of reads and writes, the length of the key (and if it is
bounded), and the distribution of key values. We must also be sure of
the cost basis. So far, we have concentrated only on the traversal
through and moving of elements as the function of the size of the
map. This is clearly not sufficient, as Andrew Bromage pointed out.


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] What is the best way to write adapters?

[oleg]

> The code is currently like this:

> instance Sig Def where
>   getName (DefClass c) = getName c
>   getName(DefProtocol p) getName p
>   getName(DefSignature s) = getName s
>   getParents(DefClass c) = getParents c
>   getParents(DefProtocol p) = getParents p
> blah blah blah...
>
> But this seems very annoying.
>
> If I have 4 different constructors in Def, and 5 methods of class Sig,
> (Please bear with me if I'm using some OO terminology because I'm still a
> new FP programmer), I'll have to write 4*5=20 forwarding functions.

Adapters seem by necessity higher-ranked functions. The following is
a stubefied code that uses generic adaptors (the function fwd).

> {-# OPTIONS -fglasgow-exts #-}
> module Foo where
>
> class Sig a where
>   getName :: a -> Int
>   getParents :: a -> String
>   getMethods :: a -> String
>
> data ClassDef = ClassDef
> data ProtocolDef = ProtocolDef
>
> instance Sig ClassDef where
> getName _ = 0
> getParents _ = "ClassDef Parents"
> getMethods _ = "ClassDef Methods"
>
> instance Sig ProtocolDef where
> getName _ = 1
> getParents _ = "ProtocolDef Parents"
> getMethods _ = "ProtocolDef Methods"
>
> data Def = DefClass ClassDef | DefProtocol ProtocolDef
>
> fwd::(forall a. Sig a => a -> w) -> Def -> w
> fwd f (DefClass c) = f c
> fwd f (DefProtocol p) = f p
>
> instance Sig Def where
> getName = fwd getName
> getParents = fwd getParents
> getMethods = fwd getMethods

Tests:

*Foo> getParents ClassDef
"ClassDef Parents"
*Foo> getParents ProtocolDef
"ProtocolDef Parents"
*Foo> getParents (DefClass ClassDef)
"ClassDef Parents"
*Foo> getParents (DefProtocol ProtocolDef)
"ProtocolDef Parents"
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Overapping instances [Was: What is the best way to write adapters?]

[oleg]

Ben Yu wrote:

> The instance declaration is like this:
> instance FwdSig Native
> instance FwdSig Def
> instance FwdSig d => Sig d
> instance Sig XXX
>
> Neither Native nor Def are direct instances of Sig.
> And this XXX, it is an instance of Sig, not a FwdSig.
>
> As you can see, there's no real overlapping at all if we take the "FwdSig d
> =>" as a precondition for "Sig d".

You have pointed out one of the most confusing issues when dealing
with typeclasses. One has the temptation to view

> class Foo a
> instance Foo Int
> instance (Real a) => Foo a
> instance Foo a

something like

> foo 5 = 
> foo a | is_real a = 
> foo a = 

But there is a great difference. The typechecker chooses which
instance to use based entirely on the shape of the types described in
the instance, disregarding the constraints. In the Foo example, if we
drop the constraints, we get

> instance Foo Int
> instance Foo a
> instance Foo a

It's immediately obvious that there is no way the compiler could choose
between the second and the third instance. And so we get a duplicate
instances error.  If we remove the third instance for example, we
still get the problem: if the type in question is Int, which instance,
the first or the second, should the compiler choose. The flag
-fallow-overlapping-instances increases the compilers's IQ and so
the compiler notices that the "Foo Int" is a specialization of "Foo
a" (that is, there exists a substitution a->Int which makes "Foo a"
identical to "Foo Int"). Therefore, if the instances can be so
ordered, the compiler chooses the most specific applicable instance.

After the compiler chose the instance, the compiler _becomes
committed_ to it.  Then the compiler notices constraints (e.g., Real
a) and checks if they are satisfied. If they are not -- the
typechecking fails. The compiler makes no attempt to choose another
instance (more general one, if any) and see if that would work
out. This is in the marked contrast with functional clauses (and with
Prolog), where the failure of a guard on one clause causes another
clause to be tried.

If the compiler had taken instance constraints into account when
choosing class instances, great many things would be possible. For
example, we could easily dispatch on a class of a type of a value.
That is, we could write
class Foo a where what_is_it:: a -> String
instance (Num a) => Foo a where what_is_it _ = "a number"
instance (Monad a) => Foo a where what_is_it = "an action"

In generally, we could implement `instanceOf' in a robust and succinct
way.

I guess history plays some part: in Haskell98, which does not permit
overlapping instances, there can be no more second chances. If the
instance constraints failed, that is it. 

I do want to point out that adding 'backtracking' to the instance
choosing algorithm isn't that trivial. The first question is: should
we permit instances that are truly duplicates, like "instance (Real a)
=> Foo a" and "instance Foo a" above. Many people would say
yes. However, we cannot tell which of these instances is more general
(syntactically, they are both "Foo a". There is generally no ordering
on constraints). So, absent of a substitution-induced ordering, we
are forced to resort to textual ordering. If two instances are
otherwise the same, the one that appears first should be tried
first. However, what does it mean to "textually appear first"? If one
instance is declared in one module and the other is in another module
(imported via a third module), which of them appears first?  We are
confronted with the eternal open/closed world issue. To see where it
can lead us, one may wish to look at the XSLT Recommendation. 
http://www.w3.org/TR/1999/REC-xslt-19991116#conflict

The XSLT processor likewise has the task of choosing the most
appropriate template. The processor has to mind 'modes', import
precedence, and even compute priorities of patterns. Curiously, the
wildcard '*' gets the priority of -0.5. Integers are not enough for
them.

I wonder if this stuff is already in HaWiki

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: concurrent haskell, higher-order types and parameterizing by typeclass

[oleg]

> data Showable = forall a. Show a => Showable a
>
> writer :: Chan Showable -> IO ()
> writer ch = mapM_ (writeChan ch) [Showable 42, Showable pi, Showable
> "hello", Showable 'c']
>
> printer :: Chan Showable -> IO ()
> printer ch = getChanContents ch >>= mapM_ (\(Showable a) -> print a)
>
> However, this solution requires a new wrapper datatype (or at least a
> new constructor) to be defined for every typeclass to be used in
> Chan-based communication; furthermore, all of the datatypes will be
> identical except for the name of the typeclass.  It seems like I
> should be able to create a type that's parameterized by typeclass,
> i.e. something like:
> data Wrapper c = forall a. c a => Wrapper a
> writer :: Chan (Wrapper Show) -> IO ()

We can do the following:

> {-# OPTIONS -fglasgow-exts #-}
>
> import Data.IORef
>
> data W r = forall a. W a (a->r)
>
> -- emulate the channel
> type Chan a = IORef [W a]
>
> writeChan ch x = do
> c <- readIORef ch
>   writeIORef ch (x:c)
>
> getChanContents ch = readIORef ch
>
> -- Channel is parameterized by the answer type!
> writer :: Chan String -> IO () 
> writer ch = mapM_ (writeChan ch) 
>[W 42 show, W pi show, W "hello" show, W 'c' show]
>  
> printer :: Chan String -> IO () 
> printer ch = getChanContents ch >>= mapM_ (\(W a h) -> putStrLn $ h a)
>
> main = do 
> ch <- newIORef []
>   writer ch
>   printer ch

That is, pack the handler along with the data. The channel is
parameterized by the answer type of the handler. Indeed, class Show
means that we can apply the function 'show' to any value of the type
in that class -- and get a string. If we use the Showable wrapper as
in the original code, applying show is _the only thing_ we can do with
that value. As we're interested in the answer type anyway (because
there is nothing else we can do with the value), we can parameterize the class
by the answer type. If we can perform several operations on the value,
we can parameterize the channel by a tuple of all answer types.

A cynic might remark that all this exercise with existentials is for
nothing: Indeed, "W x show" is precisely equivalent to just "show x".
Because of the non-strictedness, we can apply (or partially apply) all the
handlers to the value in question and pass these applications through
the channel. Only the needed ones would be evaluated.



___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Correct interpretation of the curry-howard isomorphism

[oleg]

> So, either the interpretation of the isomorphism is wrong, or Haskell
> type syste m is in fact unsound. Right ?
> They cannot be both true!

Let us indeed examine what exactly it means for a type system to be
sound. The soundness of a type system is usually proved as a theorem
of a form:
If an expression E is (statically) assigned a type T,
*AND* if the evaluation of the expression E terminates and yields
a value V of type T', then T = T'

(if the type system supports subtyping, then the theorem says that T'
is a subtype of T). Please note the second IF. In Haskell, if we don't
use unsafePerformIO [1], the theorem holds (certainly for the large
subset of Haskell that is described by the HM type system). 

Regarding Curry-Howard isomorphism: it has two parts:
- a term is an encoding of a proof of a formula that is
its type
- proof normalization corresponds to term normalization
(Thanks to Ken Shan for explaining this). 

Let us concentrate on the first part (which we would call Curry-Howard
correspondence). First of all, why it can hold. Judgments of a
type system may be considered axioms and inference rules. A formula is
a theorem if we can point out a proof, that is, a tree of axioms
and rules that lead to that formula. We also note that a type
judgment is associated with a term of a particular structure. So, we
can encode a tree of type judgments as an abstract syntax tree. That
is, a term is an encoding of a proof tree. I guess it is easy to
explain with an example:

In the following, s, t, u would be type variables (aka variables in
our logical system), x, y, z would be term variables. Greek letters
stand for meta-variables in axiom schemas and rules. Gamma is a
(perhaps empty) set of formulas. -> stands for a logical implication
and the functional arrow.

Let us attempt to prove the first-order logical formula
(s->((s->t)->t))
where -> stands for logical implication. One can construct a truth
table to see that the formula is a tautology.

We will prove it in the Sequent Calculus LK. We actually need only a
subset of the calculus' axioms and inference rules:

A: Gamma, alpha ---> alpha 
C1: Gamma, alpha ---> beta  ===> Gamma ---> alpha -> beta
C2: Gamma ---> alpha -> beta===> Gamma, alpha ---> beta

Here ---> separates the antecedent and the succedent of a sequent,
===> separates the premise and the conclusion of a rule. C1 and C2 are
actually the same rule: in LK, rules can be applied either way.

Here's the proof:

A:  s->t ---> s->t
C2: s->t ---> s->t   ===>
C1: s, (s->t) ---> t ===>
C1: s ---> (s->t)->t ===>
---> s->((s->t)->t)

Now, we can introduce terms:
exp ::= variable | \variable -> exp | exp exp
and annotate inference rules with terms:

C1: Gamma, x::alpha ---> exp::beta  ===> Gamma ---> (\x->exp)::(alpha -> beta)
C2: Gamma ---> exp::(alpha -> beta)
===> Gamma, exp2::alpha ---> (exp exp2)::beta

Now we can encode the above proof as a term (\x->\f->(f x)). Indeed,
the syntactic form of a term uniquely determines the rule to apply. So
the abstract syntax tree of a term is proof tree (for the type of a
term). We can enter
:type  \x -> (\f -> f x)
in Hugs or GHCi and see that the term has indeed the desired type.


Haskell terms and Haskell types are of course more complex. In
particular, Haskell includes the following axioms and rules:

---> [] :: alpha
---> id :: alpha -> alpha
Gamma ---> x::[alpha] ===> Gamma ---> (head x)::alpha
Gamma ---> x::(alpha->alpha) ===>
Gamma ---> (fix x) :: alpha

Using these rules, one can easily derive that
---> (head []) :: alpha
---> (fix id)  :: alpha
Indeed, if we ask a Haskell system
":type head []" or ":type fix id"
we see the result "forall a. a".
That is, we can derive everything and anything at all. The world is
trivial.

However, the above reasoning had a flaw: the rules for 'head' and
'fix' actually had side conditions. For example, the rule for 'head'
applies only if the argument of 'head' is a non-empty list. That
condition was implicit -- but it had to be verified for our proof to
be valid. Similarly, the rule for 'fix' applies only if 'fix x'
terminates. It is slighty cumbersome to express this side condition
formally. Therefore, when applied to Haskell, the Curry-Howard
correspondence has to be modified. Terms may encode invalid
proofs. Only terms that are values or that can be reduced to values in
finite number of steps encode valid proofs. Thus: a type (==formula)
is proven if there is a program (term) that evaluates to a value of
that type.

[1] Given unsafePerformIO, it is possible to implement "coerce:: a
->b" that is a terminating, total function. Here it is, for easy
reference.

coerce:: a->b
coerce a = let ref = unsafePerformIO (newIORef undefined)
   in unsafePerformIO ((writeIORef ref a) >> readIORef ref)

In a sense, a language with unsafePerformIO is akin to a theorem
prover with a 

Re: [Haskell] a newbie question

[oleg]

> I was thinking about creating a generic monad that can persist state change
> even when fail is called. The StateT monad will discard the state change so
> it makes it hard to add tracing to the program. (at least to me. If there's
> any nice way of doing this, please kindly instruct me.)

If you have (StateT m) where m is MonadIO or a ST monad, you can replace
(StateT m) with (ReaderT m). That is, you can allocate IORef and make
that IORef the (reader) environment for the further computation. The
mutations done to the IORef would not be backtracked on failure. 

In the case of an IO monad, the conversion from (StateT IO) to a
(ReaderT IO) has another important advantage. The exception handling
primitives like catch work only with IO itself (not with MonadIO). In
the case of (ReaderT IO), it is easy to strip out the environment and
get the IO itself. This is not the case with (StateT IO).


> to_write :: ((x->a)->r) -> (x->(a,s)) -> (r,s)
> to_write f1 f2 = ...
>
> I can't get a data of type x, so the only way is to pass f2 into f1. In
> order to pass f2 to f1, I have to discard the s returned by f2. Thus, I
> lose the s forever.

That is, we can only do f1 (fst . f2) to get the result 'r', Right?
The problem is getting snd . f2. I'm afraid the problem seems
to be underspecified. What if 'f1' never calls f2? What kind of value
of type 's' should we return from to_write? What if f1 calls, f2 1024
times? Which of the 's' values should we return?

I think I understand what you were trying to accomplish. 's' signifies
something like 'invocation counter'. We would like to count the number
of invocation of a specific function, without disturbing the rest of
the code. I'm afraid the most robust solution is to use IORef. If you
are not in the IO monad, you have to use unsafePerformIO then,
something like the following

to_write f1 f2 = let sr = unsafePerformIO (newIORef undefined) in
 let r = f1 (\x -> let (a,s) = f2 x in
seq (unsafePerformIO (writeIORef sr s))
a)
 in seq r (r, (unsafePerformIO (readIORef sr)))

If you compile the code, you also need to write a pragma to prevent
inlining. OTH, if the compiler does inline 'sr', you merely get an
error. If you're already in a monad, things are simpler, of course.

If the types 'r', 'x' and 'a' are in the class Num, another approach
might be plausible:

data NewNum a = NewNum a Int -- assuming that 's' of type Int
instance (Num a) => Num (NewNum a) where
  abs (NewNum a s) = NewNum (abs a) s --etc
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: how to write a list builder? fixpoint?

[oleg]

> Is it possible to write a function to build a list [a]?
> so that I can write [a,b,c,d] as "getBuilt $ build a b c d"?

Yes, in the format very close to desired. 

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module Foo where
>
> class BuildList a r  | r-> a where
> build' :: [a] -> a -> r
>
> instance BuildList a [a] where
> build' l x = reverse$ x:l
>
> instance BuildList a r => BuildList a (a->r) where
> build' l x y = build'(x:l) y

That's it. It works both on GHC and Hugs.

*Foo> build' [] True :: [Bool]
[True]
*Foo> build' [] True False :: [Bool]
[True,False]
*Foo> build' [] True False False :: [Bool]
[True,False,False]
*Foo> build' [] 'a' 'b' 'c' 'd' 'e' :: [Char]
"abcde"
*Foo> build' [] (1::Int) :: [Int]
[1]
*Foo> build' [] (1::Int) (2::Int) :: [Int]
[1,2]
*Foo> build' [] (1::Int) (2::Int) (3::Int) :: [Int]
[1,2,3]

Note that the type annotation [Bool] etc. at the end is required: it
is the delimiter of the list. Who would have thought that the type
annotation can play the role of Nil...

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: how to write a list builder? fixpoint?

[oleg]

> Another question about overloading with type classes. It seems that these
> overloaded functions cannot be passed as higher-order function. Is that
> true? A higher order function can never be overloaded?
>
> In an example, how can I pass "build" as a function to another function
> that does some algorithm? (as the traditional Builder pattern in OO term)

A function that takes a polymorphic function and uses it
polymorphically has a higher-ranked type. Higher-ranked types cannot
be inferred (in general) and must be declared explicitly. In great
detail, this question is discussed in Ken Shan's survey
http://www.eecs.harvard.edu/~ccshan/cs252/usage.pdf

As to your question: we can indeed pass 'build' to other
functions and use that argument as a function with the variable number of
arguments. Please see the function use_build in the code below. It
works both in GHC and Hugs.

P.S. Sorry I cannot reply directly to you: your ISP combined.com
blocks my mail.

{-# OPTIONS -fglasgow-exts #-}

module Foo where

class BuildList a r  | r-> a where
build' :: [a] -> a -> r

instance BuildList a [a] where
build' l x = reverse$ x:l

instance BuildList a r => BuildList a (a->r) where
build' l x y = build'(x:l) y

--build :: forall r a. (BuildList a r) => a -> r
build x = build' [] x

-- build 'a' :: String
-- build 'a' 'b' :: String
-- build (1::Int) :: [Int]
-- build (1::Int) (2::Int) :: [Int]
-- build (1::Int) (2::Int) (3::Int) :: [Int]
  
-- polyvariadic functions -- functions with the variable number of
-- arguments -- are possible in Haskell after all...

-- Higher-ranked type: the signature is required
use_build::(forall r a. (BuildList a r) => a -> r) -> x -> x -> x -> x -> [[x]]
use_build bb a b c d =
  let t1 = bb a
  t2 = bb a b
  t3 = bb a b c
  t4 = bb a b c d
  t5 = bb a b c d a
  in [t1,t2,t3,t4,t5]
  
test = use_build build 'a' 'b' 'c' 'd'

-- *Foo> test
-- ["a","ab","abc","abcd","abcda"]
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: how to write a list builder? fixpoint?

[oleg]

I'm sorry I couldn't resist another example -- which requires fewer
signatures. It also illustrates storing build in data structures.
In the example below (which works with the code posted earlier) build
is used to build itself. It really has quite a few faces...

data W = W (forall r a. (BuildList a r) => (a->r))

test2 = let t1 = build (W build)
t2 = build (W build) (W build)
t3 = t1 ++ t2
f (W b) = b (1::Int) ++
  b (1::Int) (2::Int) ++
  b (1::Int) (2::Int) (3::Int)
in map f t3

We should probably move to Cafe for further discussions, if any...

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: how to write a list builder? fixpoint?

[oleg]

Ben Yu wrote:

> I'm new to haskell, new to this group, don't even know what this
> "cafe" refers to. Is there a special place for discussing further
> details?

Yes, http://haskell.org/mailman/listinfo/haskell-cafe

>Similarly, a builder can be built for binary functions like addToFM.

Here's a bit more general variant of it:

> class Builder2 c a b r | r -> a where
>   build2 :: (a->b->c a b->c a b) -> c a b -> a -> b -> r
> instance Builder2 c k v (c k v) where
>   build2 acc seed k v = acc k v seed
> instance Builder2 c a b r => Builder2 c a b (a->b->r) where
>   build2 acc seed a b x y = build2 acc (acc a b seed) x y
>
> newtype AL a b = AL [(a,b)] deriving Show
>
> test1::AL String Bool
> test1 = build2 (\x y (AL l) -> AL $ (x,y):l) (AL []) "a" True "b" False
>
> test2:: FiniteMap String Bool
> test2 = build2 (\x y m -> addToFM m x y) emptyFM "a" True "b" False "c" True

The function build2 not only has the variable number of
arguments. These arguments don't even have to be of the same type.


> However, I don't quite like having to say buildl (1::Int). If I can say
> [1,2,3], which types to Num a => [a], why can't I say buildl 1 2 3 which
> also types to Num a => [a]?

[1,2,3] is a syntactic sugar for 1:(2:(3:[])). The operator (:) has
the type
(:) :: forall a. a -> [a] -> [a]
Since (:) is actually a function, the type of the result (which is
[a]->[a]) is unambiguously determined by the type of the argument,
'a'. Informally, the type of a function has a functional dependency. 

The function build' is a member of a class such that the type of the
result of build' unambiguously determines the type of the
argument. Note the reverse implication. Therefore, once we specify
the type of the result, everything works out. And it does:

Foo> build 1 2 3 4 :: [Int]
[1,2,3,4]

In Hugs. But not in GHC (6.0.1). My impression is that GHC assumes
overlapping instances when choosing instances -- even if no
-fallow-overlapping-instances flag is present. In order to get the
example work in GHC, we have to assure that all arguments to build
have the same type in some other way, e.g., using local type
variables:

*Foo> let (a::t)=1 in let b=(2::t); c=(3::t) in build a b c a b c ::[t]
[1,2,3,1,2,3]

The result is actually polymorphic, Num t => [t].

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] The two-class trick

[oleg]

The two-class trick helps us indirectly write desirable
multi-parameter classes with functional dependencies or
overlapping. The example below happens to have both. The example
illustrates that an attempt to write desired instances directly runs
into problems of bad overlapping or violations of functional
dependencies. The trick lets us get around those unfortunately quite
common problems.

Many if not all problems with overlapping instances can be solved with
the general approach described in the HList paper [HList]. The paper
conjectures that the overlapping instances extension itself may be
unnecessary after all.

The HList paper: http://www.cwi.nl/~ralf/HList/

The two-class trick still seems worth explaining because it gives an
example of turning an apparent drawback of the instance selection
algorithm to our advantage. In Haskell, class instances are chosen
based only on the syntactic shape of the type terms in
question. Specifically, instance constraints, if any, do _not_ affect
the instance selection. This fact is often considered one of the major
stumbling blocks to using Haskell overloading for ``logical
programming''. The instance selection algorithm is somewhat akin to the
selection of the appropriate function declaration clause. We can
influence the selection by adding a guard -- an arbitrary
boolean expression -- to a function clause. Alas, we cannot similarly
influence the selection of an instance by adding a constraint. If an
instance has a constraint, the latter is checked _after_ the
typechecker has selected and become committed to that instance. If
that constraint turns out unsatisfiable, the whole typechecking
fails. There is no backtracking: the typechecker does not attempt to
choose another instance.


This message is the complete code. Therefore, we need preliminaries

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
>
> module DelH where
>
> data HNil = HNil deriving Show
> data HCons a b = HCons a b deriving Show

A sample heterogenous list is as follows:

> l1 = HCons True $ HCons 'a' $ HCons "ab" $ HCons 'z' $ HNil

The HList paper defines infix operators that make building
heterogenous lists far more pleasant. Please see the HList paper
[HList] for much more explanations and many more operations on
heterogenous lists.


Our goal here is to write a function |hdel| that deletes the first
occurrence of an element of a given type from a given heterogeneous
list. For example,

> test1 = hdel 'x' l1

will delete the first element of the type |Char| from the list |l1|:

  *DelH> l1
  HCons True (HCons 'a' (HCons "ab" (HCons 'z' HNil)))
  *DelH> test1
  HCons True (HCons "ab" (HCons 'z' HNil))

The given list must contain at least one element of the desired type.
Otherwise, it is a type error.

We can start by writing

> class HDeleteFst e l l' | e l -> l' where
>hdel:: e -> l -> l'

> instance HDeleteFst e (HCons e l) l where
>hdel _ (HCons _ l) = l


At first, the code is quite straightforward: if we see the occurrence
of the desired element type in the head of |HList|, we return the tail
of the list. We are tempted to write the second case (when the desired
element type is not in the head of the list) as follows

*> instance HDeleteFst e l l' =>
*>  HDeleteFst e (HCons e' l) (HCons e' l') where
*>hdel e (HCons e' l) = HCons e' (hdel e l)

Alas, that does not work. The most general unifier of the instances
HDeleteFst e (HCons e l)  l
and
HDeleteFst e (HCons e' l) (HCons e' l')
is
e' -> e, l -> (HCons e l')

The unifier exists, therefore, the instances do overlap.  However, there
is no such substitution that, when applied to the second instance
makes it identical to the first, nor vice versa. So, the instances are
unifiable but not comparable -- and the compiler will complain.

The trick is to introduce a helper class

> class HDeleteFst' e l l' | e l -> l' where
>hdel':: e -> l -> l'

which is in all respect similar to the first class. Now, we add a
relaying instance of |HDeleteFst|:

> instance HDeleteFst' e l l' => HDeleteFst e l l' where
>hdel = hdel'

As we can see, the two instances of our class, 
|HDeleteFst e (HCons e l1) l1| and |HDeleteFst e l l'| still
overlap. Now, the former is strictly more specialized than the latter,
because there exists a substitution |l -> (HCons e l1), l -> l1|,
which, when applied to the general instance makes it identical to the
former instance. GHC no longer complains because now the overlapping 
instances are ordered and so the compiler can choose the right one.

We still need to add an instance for the new class |HDeleteFst'|

> instance HDeleteFst  e l l' =>
>  HDeleteFst' e (HCons e' l) (HCons e' l') where
>hdel' e (HCons e' l) = HCons e' (hdel e l)

Modulo the substitution |HDeleteFst'| for |HDeleteFst| and
|hdel'| for |hdel|, this is precisely the instance we wanted -- but
could not write be

[Haskell] Re: closure of coercions with classes

[oleg]

> The guts of the question is: can one use the class system to code up
> the reflexive, transitive closure

Computing the transitive closure of types is possible:
http://www.haskell.org/pipermail/haskell-cafe/2003-October/005249.html
http://www.haskell.org/pipermail/haskell-cafe/2003-November/005433.html

>   pair :: STRef ((s1, s2), s3) a ->
>   STRef (s1, s2) b ->
>   ST (((s1, s2), s3), s4) (STRefr1 (a, b))
>
> which isn't as general as I would like, as it imposes a particular order
> on the nested scopes.  

That problem could be solved by open sums, it seems. The HList paper
showed how to achieve that, in current Haskell.

> I've experimented with a few different attempts, but in the best case
> succeeded only in exhausting stack space while searching for satisfying
> instances.

Could it be possible to post the complete code for those attempts? I'd
like to try a few tricks to avoid the divergence.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Exceptions in types and exception-free programming

[oleg]

S. Alexander Jacobson wrote:
>   Also, is there a way to get the typesystem to
>   tell you which functions may fail i.e. which
>   functions have failMsg as an implicit parameter?


Generally speaking, that is not that easy. If we have a functional
composition (foo . bar), we wish its type to reflect the _union_ of
exceptions that can be raised in 'foo' and in 'bar'. Union types are
hard to get. That's why in Ocaml, for example, exceptions aren't the
part of a function signature.

The good news is that we already have union types in Haskell -- to a
large extent. To an extent enough to put exceptions into the
types. The following are two approaches. They aren't perfect -- but
that's a start. A better way however is to statically assure that no
exception can occur. That is possible to achieve in Haskell today --
and improve efficiency of the code in the process due to elimination
of run-time checks. The end of the message gives an example.


The first approach applies only to polymorphic functions. Also we have
to watch for monomorphic restriction (but we all know that). And it
also works in GHC only, because GHC is lazy when it comes to
constraint resolution (which is a good thing, IMHO).

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module TER where
>
> class CERROR a c where
> darn:: a -> c-> String -> b
>
> instance Show a => CERROR a c where
> darn label _ msg = error $ "Error: " ++ (show label) ++ " " ++ msg
>   
>
> data EHead = EHead deriving Show
> data ETail = ETail deriving Show
> data EJust = EJust deriving Show
>
> myhead x@([]) = darn EHead x "head of an empty list"
> myhead (x:_) = x
>
> mytail x@([]) = darn ETail x "tail of an empty list"
> mytail (_:xs) = xs

Now, if we ask GHCi for the type of myhead, we get

*TER> :t myhead
myhead :: forall a. (CERROR EHead [a]) => [a] -> a

As we can see, the exception is apparent right in the function type.
We can define

> ht x = myhead $ mytail $ mytail x

*TER> :t ht
ht :: forall a. (CERROR ETail [a], CERROR EHead [a]) => [a] -> a

We can see that we indeed have a union of exceptions that can be
raised in different sub-expressions of ht.

A more involved example:

> myjust (Just a) = a
> myjust x = darn EJust x "Just nothing"
>
> foo x = myjust $ myhead $ mytail $ myjust x


*TER> :t foo
foo :: forall b.
   (CERROR EJust (Maybe [Maybe b]),
CERROR ETail [Maybe b],
CERROR EHead [Maybe b],
CERROR EJust (Maybe b)) =>
   Maybe [Maybe b] -> b
*TER> foo (Just [Nothing,Just 2])
2
*TER> foo (Just [Nothing])
*** Exception: Error: EHead head of an empty list


The second method involves the use of implicit parameters. It works
both in GHC and in Hugs, and can work with monomorphic functions
too. But is has some other drawback (although that depends on the
point of view)

> idarn _ msg = error msg
>
> myhead1 [] = idarn ?e_head "head of an empty list"
> myhead1 (x:_) = x
>
> mytail1 x@([]) = idarn ?e_tail "tail of an empty list"
> mytail1 (_:xs) = xs
>
> ht1 x = myhead1 $ mytail1 $ mytail1 x

If we check for the type of ht1 (e.g., in Hugs), we get

TER> :t ht1
ht1 :: (?e_tail :: a, ?e_head :: b) => [c] -> c

That is, ht1 can fail because it tries to get either the head or the
tail of an empty list. Again, we get the true _union_ of exceptions.

Alas, we can't invoke ht1 in a simple way any more. We've got to bind the
errors.

TER> let ?e_head = undefined; ?e_tail = undefined in ht1 [1,2]
Program error: head of an empty list
TER> let ?e_head = undefined; ?e_tail = undefined in ht1 [1,2,3]
3


It seems that the best way to cope with exceptions is to assure
statically that they cannot occur at all -- in large segments of code.
We don't need to change Haskell. Haskell already can "fake it" quite
believably. 

Indeed, let us consider a segment of the code

assert x msg = if x then (not x) else error msg

foo x | assert (not (null x)) "non-empty-list in ..." = undefined
foo x = ... body_foo x ...

Obviously, when the second clause is about to executed, _we_ know that
x is a non-empty list. Alas, that fact is not reflected in the type of
x. And it cannot in the above case. Indeed, what if we change the
order of clauses by mistake:

foo x = ... body_foo x ...
foo x | assert (not (null x)) "non-empty-list in ..." = undefined

To the typechecker, the order of clauses makes no difference. Yet it
does to the executioneer. There is however a way to make the assurances
statically certain. We should re-write the code as

with_non_empty_list x foo

where
with_non_empty_list:: [a] -> NonemptyList [a]

does the run-time check -- and generates the run-time error. But, if
the check succeeded, we know that the list is not empty. That
information can be encoded statically, and be used within the body of
foo.  If NonemptyList is a newtype, no run-time overhead

[Haskell] Re: type class does not compile

[oleg]

Ben Yu wrote:

> class Rule r u u' m where
>   apply :: r -> u -> m u'
>
> data And = And
>
> data Bin a b o = Bin a b o
>
> instance (Monad m, Rule r1 u u' m, Rule r2 u' u'' m) => 
>  Rule (Bin r1 r2 And) u u'' m where
>   apply (Bin r1 r2 _) u = apply r1 u >>= apply r2
>
> Ghc complains about "Could not deduce (Rule r1 u u'1 m, Rule r2 u'1 u''
> m)", but it is obviously same as the constraint I gave in the instance
> declaration.

This is like the famous show . read problem. Here, 'apply r1 u'
produces the value of a type `m v' for _some_ v. and 'apply r2'
consumes this value. There is no way for the compiler to figure out
what this 'v' is. You specified 'Rule r1 u u' m' as a
constraint. However, there is nothing that guarantees that your u' in
the constraint is the same as v that is needed to resolve the
overloading. So, we need either a functional dependency, or a resort
to nifty local type variables. The example of the latter is

> instance (Monad m, Rule r1 u u' m, Rule r2 u' u'' m) => 
>  Rule (Bin r1 r2 And) u u'' m where
>   apply (Bin r1 r2 _) u = ((apply r1 u)::m u') >>= apply r2

which makes your code compile.

For more detail, please see:
http://www.haskell.org/pipermail/haskell/2003-September/012782.html
http://www.haskell.org/pipermail/haskell/2003-October/012783.html
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Eliminating Array Bound Checking through Non-dependent types

[oleg]

There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be replaced with nested tuples), on
general recursion, on annotation-free programming, on clarity of code,
on well-supported programming languages. That does not have to be the
case. This message shows a non-trivial example involving native
Haskell arrays, index computations, and general recursion. All arrays
indexing operations are statically guaranteed to be safe -- and so we
can safely use an efficient unsafeAt provided by GHC seemingly for
that purpose. The code is efficient; the static assurances cost us no
run-time overhead. The example uses only Haskell98 + higher-ranked
types. No new type classes are introduced. The safety is based on:
Haskell type system, quantified type variables, and a compact
general-purpose trusted kernel.

Our example is `bsearch', taken from the famous paper "Eliminating
Array Bound Checking Through Dependent Types" by Hongwei Xi and Frank
Pfenning (PLDI'98).  Hongwei Xi's code was written in SML extended
with a restricted form of dependent types. Here is the original code
of the example (taken from Figure 3 of that paper, see also
http://www-2.cs.cmu.edu/~hwxi/DML/examples/)


] datatype 'a answer = NONE | SOME of int * 'a
]
] assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a
] assert length  <| {n:nat} 'a array(n) -> int(n)
]
] fun('a){size:nat}
] bsearch cmp (key, arr) =
] let
] fun look(lo, hi) =
] if hi >= lo then
] let
] val m = (hi + lo) div 2
] val x = sub(arr, m)
] in
] case cmp(key, x) of
] LESS => look(lo, m-1)
]   | EQUAL => (SOME(m, x))
]   | GREATER => look(m+1, hi)
] end
] else NONE
] where look <|
] {l:nat, h:int | 0 <= l <= size /\ 0 <= h+1 <= size } int(l) * int(h) 
] -> 'a answer
] in
] look (0, length arr - 1)
] end
] where bsearch <| ('a * 'a -> order) -> 'a * 'a array(size) -> 'a answer

The text after `<|' are dependent type annotations. They _must_ be
specified by the programmer -- even for internal functions such as
`look'.

Here's our code, deliberately written to be as close to Hongwei Xi's
code as possible (This message is the complete code):

> {-# OPTIONS -fglasgow-exts #-}
> module Dep where
> import Data.Array
>
> bsearch cmp (key, arr) = brand arr (\arr' -> bsearch' cmp (key, arr'))
>
> bsearch' cmp (key,arr) = look lo hi
>  where
>   (lo,hi) = bbounds arr
>   look lo hi = let m = bmiddle lo hi
>x = arr !. m
>  in case cmp (key,x) of
> LT -> bpred lo m (look lo) Nothing
> EQ -> Just (unbi m, x)
> GT -> bsucc hi m (\m' -> look m' hi) Nothing

This code is just as algorithmically efficient as the Dependent SML
code: one middle index computation, one element comparison, one index
comparison, one index increment or decrement per iteration. There are
no type annotations as none are needed. Operator (!.) is a statically
safe array indexing operator. The type system and the trust properties
of the kernel below guarantee that in the expression "arr !. m" the
index `m' is positively in range of the array `arr' bounds.

> barr1 = listArray (5,5 + (length s)-1) s where s = "abcdefgh"
> btest1 = bsearch (uncurry compare) ('c',barr1)
> btest2 = bsearch (uncurry compare) ('x',barr1)


The code relies on a compact general-purpose trusted kernel explained
below. That code should be preferably put into a separate module.

First we introduce tags for Branded arrays and Branded indices:

> -- those two must *not* be exported!
> newtype BArray s i a = BArray (Array i a)
> newtype BIndex s i   = BIndex i
>
> unbi (BIndex i) = i

These are `newtype's and so impose no run-time overhead. Of interest
is a phantom type variable 's', which marks a _brand_ of an array and
of an array index. An index is branded if it is certainly within the
range of the array of its brand. The type variable 's' is similar to
that in the ST monad. The latter relies on 's' to enforce
serialization. We, OTH, do not impose any linearity constraints on 's'
-- it may be freely duplicated (see bbounds below) and discarded (see
`unbi'). It is created however under controlled conditions.  The
safety depends on the trusted way of creating branded types: the
constructors BIndex and BArray should be used in the trusted kernel
only, and should not be available anywhere else.  The uniqueness of 's'
afforded by the explicit universal quantification prevents mixing up of
different brands.

We must re-iterate that safety depends on assurances of the code that
constructs BIndex values. Because of the high assurance, we must
formulate the safety properties as propositions, and prove
t

Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types

[oleg]

Hello!

> What if I don't trust your kernel? The guarantees you require of
> your kernel are not statically checked. What guarantee do I have
> that the propositions which you identify are even the ones which
> are really needed to eliminate bounds checking? How does the
> machine replace ! by unsafeAt reliably, all by itself?
>
> Yes, you can convince _me_ that something of the sort will do, because
> I can follow the math. But what is the mechanism? What is the evidence?
> What's the downloadable object that can be machine-checked to satisfy
> my paranoid insurance company?

That is very well said! I hope that you can forgive me if I reply by
quoting the above two paragraphs back to you, with the substitution 
s/kernel/compiler/.

What if I don't trust your compiler?

I have heard a similar question asked of J. Strother Moore and
J. Harrison. J. Strother Moore said that most of ACL2 is built by
bootstrapping, from lemmas and strategies that ACL2 itself has
proven. However, the core of ACL2 just has to be trusted. ACL2 has
been used for quite a while and so there is a confidence in its
soundness. Incidentally, both NSA and NIST found this argument
persuasive, when they accepted proofs by ACL2 as evidence of high
assurance, in awarding Orange book A1 and IFIPS 140-1 ratings -- the
highest security ratings -- to some products.

> Hongwei Xi's code contains the evidence I'm asking for.
> The verification conditions are added by hand in the program as
> annotations, just as yours are annotations outside the program.  His
> are checked by Presburger arithmetic, just as yours could be.

Actually, as far as the PLDI'98 paper is concerned, they specifically say
they do not use the full Presburger arithmetics. Rather, they solve
the constraints by Fourier variable elimination. Anyway, even if
the various elaboration and decision rules are proven to be sound and
complete, what is the evidence that their implementation in the
extended SML compiler is also sound and complete? Speaking of
completeness, the procedure in PLDI'98 paper notes, "Note that we have
been able to eliminate all the existential variables in the above
constraint. This is true in all our examples, but, unfortunately, we
have not yet found a clear theoretical explanation why this is so."
The conclusion specifically states that the algorithm is currently
incomplete.


> ...this proposition is false. The bounds function returns bounds which
> are outside the range of the array when the array is empty.
> You'll notice that Hongwei Xi's program correctly handles this case.
>
> Don't get me wrong: I think your branded arrays and indices are a very
> good idea. You could clearly fix this problem by Maybe-ing up bbounds
> or (better?) by refusing to brand empty arrays in the first place.

I have noticed that the branding trick would work very well with
number-parameterized types. The latter provide missing guarantees, for
example, statically outlaw empty arrays. Hongwei Xi's code has another
neat example: a dot product of two arrays where one array is
statically known to be no longer that the other. Number-Parameterized
types can statically express that inequality constraint too. The
Number-Parameterized types paper considers a more difficult example --
and indeed the typechecker forced me to give it a term that is
verifiably a proof of the property (inequality on the sizes) stated in
term's inferred type. The typecheker truly demanded a proof; shouting
didn't help.

Incidentally, the paper is being considered for JFP, I guess. I don't
know if the text could be made available. I still can post the link to
the code:
http://pobox.com/~oleg/ftp/Haskell/number-param-vector-code.tar.gz

I should emphasize that all proper examples use genuine Haskell arrays
rather than nested tuples. Yet the type of the array includes its
size, conveniently expressed in decimal notation. One can specify
arithmetic equality and inequality constraints on the sizes of the
array, in the type of the corresponding functions. The constraints can
be inferred. One example specifically deals with the case when the
sizes of those arrays are not known until the run-time -- moreover,
change in the course of a computation that involves general
recursion. It seems that branding trick nicely complements
number-parameterized arrays and makes `dynamic' cases easier to
handle.


> You'll notice that Hongwei Xi's program correctly handles this case.

But what if I specified the dependent type with a mistake that
overlook the empty array case? Would the dependent ML compiler catch
me red-handed? In all possible cases? Where is the formal proof of
that?

 
I have failed to emphasize the parallels between Hongwei Xi's
annotations and the corresponding Haskell code. What Hongwei Xi
expressed in types, the previo

Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types

[oleg]

Hello!

Bjorn Lisper wrote:

> What is the relation to the sized types by Lars Pareto and John Hughes?

It is orthogonal and complementary, as the message in response to
Conor T. McBride indicated.

> What is the relation to classical range analyses for (e.g.) array index
> expressions, which have been known for a long time for imperative languages?

It is just like the classical range analysis, but _reified_ in the
programming language itself. Given a piece of code:

finda x arr = loop lo
where (lo,hi) = bounds arr
  loop i = if i <= hi then
  if x == arr ! i then Just i
  else loop (i + 1)
   else Nothing

the analysis sees that 'i' starts at the lower bound of 'arr' and is
incremented afterwards. When the analysis sees the test "i <= hi" it
infers that in the `then' branch of that test `i' does not exceed the
upper bound of the array. Therefore, the indexing operation `arr ! i'
is safe and no range check is needed.

In the `branding' framework, the programmer makes the result of the
test "i <= hi" and the corresponding implication that `i' is in range
known to the type system, by branding the index `i'. To be more
precise, the programmer would replace the first `if' statement with
if_in_range:: (Ix i) => i -> BArray s i e -> (BIndex s i->r)
  -> r ->r
if_in_range i arr on_within_range on_outside_rage ...
If `i' turns out to be in range, that fact would be recorded by
passing to the continuation on_within_range a branded index. Thus the
logical implication that was implicit in the range checker is made
explicit to the typechecker here.

> A program analysis like range analysis is not exact, of course: it must make
> safe approximations sometimes and will sometimes say that an array index
> might be out of bounds when it actually won't. In your framework, this seems
> to correspond to the fact that you must verify your propositions about index
> expressions.

True, just as the range analysis must verify the rules of the
analysis. The difference is that the conventional range analyzer is a
part of the _compiler_, typically hidden from view (of a regular
programmer). Here, the analyzer is a part of a _library_.

It is also true that our analysis can't be exact: if the code includes 
let i = very_complex_function j
and we know that j is in range, it may be very difficult to ascertain
that 'i' will always be in range. In that case, we do the following
let j_unbranded = unbrand j
i = very_complex_function j_unbranded
in if_in_range i arr on_within_range on_outside_rage

That is, we intentionally forget the branding information, do a
complex index transformation, followed by a run-time witnessing to
recover the branding. If we somehow know that very_complex_function
keeps its result in range, we can replace `on_outside_rage' with the
function that raises an exception, crashes the computer, etc. If we
are not sure if `i' is in range, then our program 
must do the range check anyway; if `i' turns out of range, the
program should do what the algorithm prescribes in that case. The
upshot is that `if_in_range' makes the programmer explicitly consider the
consequences of the range check. We turn the range check from a
routine safety check into an algorithmically significant decision.

Incidentally, if we can prove that `very_complex_function' leaves the
index in range, then we can make the function return a branded index,
and thus eliminate the if_in_range check above. Because the creation
of a branded index can only be done in a trusted kernel, we must put
such a function into the kernel, after the appropriate rigorous
verification -- perhaps formal verification.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Keyword arguments

[oleg]

We show the Haskell implementation of keyword arguments, which goes
well beyond records (e.g., in permitting the re-use of
labels). Keyword arguments indeed look just like regular, positional
arguments. However, keyword arguments may appear in any
order. Furthermore, one may associate defaults with some keywords; the
corresponding arguments may then be omitted. It is a type error to
omit a required keyword argument. The latter property is in stark
contrast with the conventional way of emulating keyword arguments via
records. Also in marked contrast with records, keyword labels may be
reused throughout the code with no restriction; the same label may be
associated with arguments of different types in different
functions. Labels of Haskell records may not be re-used.  Our solution
is essentially equivalent to keyword arguments of DSSSL Scheme or
labels of OCaml.

Keyword argument functions are naturally polyvariadic: Haskell does
support varargs! Keyword argument functions may be polymorphic. As
usual, functions with keyword arguments may be partially applied. On
the downside, sometimes one has to specify the type of the return
value of the function (if the keyword argument function has no
signature -- the latter is the norm, see below) -- provided that the
compiler cannot figure the return type out on its own. This is usually
only the case when we use keyword functions at the top level (GHCi
prompt).

Our solution requires no special extensions to Haskell and works with
the existing Haskell compilers; it is tested on GHC 6.0.1. The
overlapping instances extension is not necessary (albeit it is
convenient).

The gist of our implementation is the realization that the type of a
function is a polymorphic collection of its argument types -- a
collection that we can traverse. This message thus illustrates a
limited form of the reflection on a function.


Our implementation is a trivial extension of the strongly-typed
polymorphic open records described in
http://homepages.cwi.nl/~ralf/HList/

In fact, the implementation relies on the HList library.  To run the
code (which this message is), one needs to download the HList library
from the above site.

The HList paper discusses the issue of labels in some detail. The
paper gives three different representations. One of them needs no
overlapping instances and is very portable. In this message, we chose
a representation that relies on generic type equality and therefore
needs overlapping instances as implemented in GHC. Again, this is
merely an outcome of our non-deterministic choice. It should be
emphasized that other choices are possible, which do not depend on 
overlapping instances at all. Please see the HList paper for details.

> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> 
> module KW where
> 
> import FakePrelude hiding (TypeEq,typeEq,proxyEq,TypeCast,typeCast)
> import TypeEqGeneric2
> import TypeCastGeneric2
> import HListPrelude


We will be using an example inspired by a graphics toolkit -- the area
which really benefits from keyword arguments. We first define our
labels and useful datatypes

> data Color = Color
> data Size  = Size
> data Origin  = Origin
> data RaisedBorder = RaisedBorder
>
> data CommonColor = Red | Green | Blue deriving Show
> data RGBColor = RGBColor Int Int Int deriving Show

and two functions:

> make_square Size n Origin (x0,y0) Color (color::CommonColor) =
>   unwords ["Square:", show n, "at", show (x0,y0), show color] ++ "\n"
> 
> make_rect Size (nx,ny) Origin (x0,y0) Color (color::RGBColor)
>RaisedBorder border =
>   unwords ["Rectangle:", show (nx,ny), "at", show (x0,y0),
>  show color, if border then "raised border" else ""] ++ "\n"


We are not interested in really drawing squares and rectangles
here. Therefore, make_square and make_rect return a String, which we
can regard as a ``command'' to be passed to a low-level graphics
library. The functions make_square and make_rect are genuine functions
and can be used as such. They are not keyword argument functions, yet,
but they set the stage. These functions can be considered an
`interface' for the keyword argument functions. We should note that
the functions are polymorphic: for example, `Size' can be any
showable. We must also emphasize the re-use of the labels: The Color
of a square is the value of the enumerated type CommonColor. OTH, the
color of the rectangle is given as an RGB triple. The sizes of the
square and of the rectangle are specified differently too, the same
label notwithstanding.

Once the user wrote the functions such as make_square and make_rect,
he can _automatically_ convert them to their keyword
alternatives. This transformation is done by a function 'kw'. The user
should pass the positional-argument function (`labeled' as above),
and an HList of default values for some of the labels. The latter may
be HNil if all keyword arguments are required.

The first example (n

[Haskell] Re: Dependent Types in Haskell

[oleg]

Martin Sulzmann stated the goal of the append exercise as follows:

] Each list carries now some information about its length.
] The type annotation states that the sum of the output list
] is the sum of the two input lists.

I'd like to give a Haskell implementation of such an append
function, which makes an extensive use of partial signatures and, in
generally, relies on the compiler to figure out the rest of the
constraints. We also separate the skeleton of the list from the type
of the list elements.

This solution differs from the Haskell solution append3.hs given in
Martin Sulzmann's message. The latter solution relies on the trusted
kernel: the equality datatype E. It is quite easy to subvert
append3.hs if we set up E with particular run-time values. The error
will not be discovered statically -- nor dynamically for that matter,
in the given code. We can get the function app to produce a non-bottom
list value whose dynamic size differs from its size type (and whose
static size is patently not the arithmetic sum of the static sizes of
the arguments).

The solution in this message relies entirely on Haskell type system;
there are no trusted terms. An attempt to write a terminating term
that is to produce a list whose length differs from that stated in the
term's type will be caught by the type checker at compile time.

> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
>
> module LL where
>
> data Z; data S a

First we state the Sum constraint:

> class Add n m p | n m -> p
> instance Add Z a a
> instance Add n (S m) p => Add (S n) m p

Now we derive a number-parameterized list. We separate the shape
type of the list from the type of the list elements:

> data Nil  len a = Nil deriving Show
> data Cons b len a = Cons a (b a) deriving Show

The constraint `List f' holds iff f is the shape type of a valid list:

> class List ( lst :: * -> * )
> instance List (Nil Z)
> instance (Add (S Z) n m, List (tail n)) => List (Cons (tail n) m)

The following `type function' makes sure that its argument is a valid
list. That guarantee is established statically. We should note
that the class List has no members. Therefore, the only terminating term
with the signature `(List f) => f a -> f a' is the identity.

> make_sure_it_is_a_list:: (List f) => f a -> f a
> make_sure_it_is_a_list = id

> nil:: Nil Z a
> nil = Nil

We let the compiler write out the constraints for us:

> consSig :: a -> f l a -> Cons (f l) (S l) a
> consSig = undefined
> cons h t | False = consSig h t
> cons h t = make_sure_it_is_a_list$ Cons h t

We can create a few lists:

> testl1 = cons (3::Int) ( cons (2::Int) ( cons (1::Int) nil ) )
> testl2 =   ( cons (2::Int) ( cons (1::Int) nil ) )

The type of testl2 is reasonable:

testl2 :: Cons (Cons (Nil Z) (S Z)) (S (S Z)) Int

If we try to cheat and write
 consSig :: a -> f l a -> Cons (f l) (S (S l)) a
the typechecker will point out that 'Z' is not equal to 'S Z' when
typechecking testl1 and testl2.

We can now handle Append:

> class Append l1 l2 l3 | l1 l2 -> l3 where
> appnd :: l1 a -> l2 a -> l3 a
>
> instance Append (Nil Z) l l where
> appnd _ l = l
>
> instance (Append (t n) l (t' n'), List (t' n'))
> => Append (Cons (t n) (S n)) l (Cons (t' n') (S n')) where
> appnd (Cons h t) l = cons h (appnd t l)
 
We had to be explicit with types in the latter instance. The types
must correspond to the term; the typechecker will tell us if they do
not.

We now attempt to verify the sum of lengths property. We attach the
desired constraints using the partial signature trick. This saves us
trouble enumerating all other constraints.

> constraintAdd:: Add l1 l2 l3 => (f1 l1 a) -> (f2 l2 a) -> (f3 l3 a)
> constraintAdd = undefined

> vapp l1 l2 | False = constraintAdd l1 l2
> vapp l1 l2 = appnd l1 l2

Perhaps we should move to Cafe?
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Applicative translucent functors in Haskell

[oleg]

ML is known for its sophisticated, higher-order module system, which
is formalized in Dreyer-Crary-Harper language. A few months ago Ken
Shan showed a complete translation of that language into System Fw:

http://www.eecs.harvard.edu/~ccshan/xlate/

Ken Shan has concluded that languages based on Fw, such as Haskell
with common extensions, already support higher-order modular
programming. In fact, his paper showed a sample Haskell translation of
the most complex and interesting ML module expression: a translucent,
applicative functor. Different instantiations of the functor with
respect to type-compatible arguments are type-compatible; and yet the
functor hides the representation details behind the unbreakable
abstraction barrier.

Dreyer-Crary-Harper language and System Fw are deliberately
syntactically starved, to simplify formal analyses. Therefore, using
the results of Ken's paper _literally_ may be slightly
cumbersome. This message is an attempt to interpret some of Ken's
results in idiomatic Haskell with the full use of type classes. We
will also show that type sharing constraints can be expressed in a
scalable manner, so that the whole translation is practically
usable. Thus we can enjoy the sophisticated, first-class higher-order
module system in today's Haskell. No new extensions are required;
furthermore, even undecidable instances (let alone overlapping
instances) are not used. This message has been inspired by Ken Shan's
paper and has greatly benefited from several conversations with him.


Throughout this message we will be using an example of polymorphic
sets parameterized by an element-comparison function. Our example is
an extended version of the example in Ken's paper. We will also be
using OCaml syntax for module expressions, which, IMHO, makes a little
bit more sense.  We abuse the terminology and use the word 'module' to
also mean what ML calls 'structure'.

This message is both Haskell and OCaml literate code. It can be loaded in
GHCi or Hugs -98 as it is. To get the OCaml code, please filter the text
of the message with "sed -n -e '/^}/ s/^} //p'"

> {-# OPTIONS -fglasgow-exts #-}
> module Functors where

Our goal in this message is to produce implementations of a SET
interface:

} module type SET = sig
}   type element
}   type set
}   val empty  : set
}   val add: element -> set -> set
}   val member : element -> set -> bool
} end;;

This is the OCaml declaration of a type of a collection made of two
type declarations and three value declarations. Such collections are
called structures (or, modules, by abuse of the terminology) and
their types are called signatures. The concise description of the
OCaml module language can be found at

http://caml.inria.fr/ocaml/htmlman/manual004.html

We should point out that the types 'element' and 'set' are abstract --
the right-hand side of the corresponding type declarations is
empty. In ML, a single colon adds a type annotation whereas a double
colon is a list constructor -- in Haskell, it is just the opposite.
The corresponding SET signature in Haskell is well-known:

> class SET element set | set -> element where
> empty  :: set
> add:: element -> set -> set
> member :: element -> set -> Bool

We shall build an implementation of SET parameterized by the element
comparison function. The comparison function's interface is to be
described by its own signature, ORD. We shall define two different
instances of ORD and instantiate the SET functor with those two
instances. To make the game more interesting, our implementation of
the ORD interface will itself be parameterized by the ENUM interface,
which maps elements in a totally ordered domain into integers. So, the
comparison function will use that mapping to derive the element
comparison. Thus our game plan is: 
  - introduce the ENUM interface, 
  - define two implementations of the ENUM interface,
  - introduce two different ENUM->ORD transparent functors,
  - instantiate the functors yielding four implementations of the
ORD interface,
  - introduce a translucent ORD->SET applicative functor,
  - instantiate it obtaining different implementations of SET
  - run a few tests, to illustrate applicativity of the functor and
the abstraction barrier

We start with the ENUM interface:

} module type ENUM = sig
}   type e
}   val fromEnum: e -> int
} end;;

and its two implementations. One of them is

} module IntEnum : (ENUM with type e = int) = struct
}   type e = int
}   let fromEnum x = x
} end;;

We wrote a module expression -- a collection of one type definition
and one (functional) value definition, and told the compiler its
explicit type, ENUM. The stuff after 'with' is a type sharing
constraint: the type of IntEnum is ENUM such that the type ENUM.e is
int. The explicit type annotation can be dropped:

} module CharEnum = struct
}   type e = char
}   let fromEnum x = Char.code x
} end;;


The corresponding code in Haskell is
  

Indeed, the standard En

Re: [Haskell] GHC / Hugs Disagree on Constraints

[oleg]

Dominic Steinitz wrote:

> Did you get the first solution to work? When I tried it with hugs -98 I got

Yes, in the process discovering some interesting behavior of
Hugs. Here's the complete code that works with Hugs

> module Foo where
>
> class Bits a
>
> instance (Ord a, Bits a, Bounded a, Integral a,
>  Bits b, Bounded b, Integral b) =>
> Bounded (LargeKey a b) where
>minBound = 0
>(maxBound :: (LargeKey a b)) =
>  (fromIntegral::Int->(LargeKey a b)) $
>  (1 + fromIntegral (maxBound::b))*
>(1 + fromIntegral (maxBound::a)) - 1
> data LargeKey a b = LargeKey a b deriving (Eq, Ord,Show)
> instance (Ord a, Eq a, Ord b, Show a, Show b) =>
> Num (LargeKey a b) where
>(+) = undefined
>fromInteger = undefined

There are two interesting points: first, in order to add a type
annotation to the result of a function, we have to place the whole
function head in parenthesis, as in
(maxBound :: (LargeKey a b)) = ...
That does confuse GHC and cause it to give some quite weird error
message. So, with parenthesis, it works in Hugs -98 but not in
GHC. Without the parenthesis, it works the other way around.

The other issue is an unnecessary type annotation on the function
fromIntegral. GHC works well without that annotation. Alas, Hugs
(November 2003) reports
INTERNAL ERROR: findBtyvsInt

The second solution seems better: not only it is in Haskell98, it also
agrees with both Haskell systems.


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] GHC / Hugs Disagree on Constraints

[oleg]

> instance (Ord a, Bits a, Bounded a, Integral a, LargeWord a,
>   Bits b, Bounded b, Integral b, LargeWord b) =>
> Bounded (LargeKey a b) where
>minBound = 0
>maxBound =
>   fromIntegral $
>   (1 + fromIntegral (maxBound::b))*
>  (1 + fromIntegral (maxBound::a)) - 1
>
> Hugs rejects it with +N -98 with

One fix is to bring type variables into the local scope, for
example,

> instance (Ord a, Bits a, Bounded a, Integral a, LargeWord a,
>   Bits b, Bounded b, Integral b, LargeWord b) =>
> Bounded (LargeKey a b) where
>minBound = 0
>maxBound :: (LargeKey a b) =
>   fromIntegral $
>   (1 + fromIntegral (maxBound::b))*
>  (1 + fromIntegral (maxBound::a)) - 1

You still need -98 flag for Hugs. Another solution is totally
Haskell98: introduce two functions

> aoflk:: (LargeKey a b) -> a; aoflk = undefined
> boflk:: (LargeKey a b) -> b; boflk = undefined

then maxBound can be implemented as

>maxBound = result where
>  result =
>   fromIntegral $
>   (1 + fromIntegral (maxBound `asTypeOf` (boflk result)))*
>  (1 + fromIntegral (maxBound `asTypeOf` (aoflk result))) - 1

The apparent recursion in the above definition is superficial. The
definition isn't actually recursive. We merely need the type of the
'result' rather than its value.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: threading mutable state through callbacks

[oleg]

Jules Bean wrote:
> Unfortunately, it's not going to work. It's not going to work because
> some of the procedures take callbacks, and the callbacks are values of
> type IO (). I can see two solutions to this:
>
> a) revert to using an IORef, and use lexical scoping to define my
> callbacks in a location such that the reference to the environment is
> in scope.  This will work, but it's just not convenient to define all
> your functions inside another function so you can do a lexical scoping
> trick...
>
> b) write the callbacks as values of type
>
> StateT Env IO ()
>
> Is this the right approach? Is there a better one?

Yes: implicit parameters and implicit configurations. The end user code
is often identical in both of these approaches (but the latter may
require a bit more preparation. OTH, implicit parameters are supported
by the compiler whereas the latter is just a Haskell library). Both
approaches are compared in Appendix A of the paper

http://www.eecs.harvard.edu/~ccshan/prepose/prepose.pdf

The example is writing JNI functions in Haskell. Incidentally, the
example illustrates passing of the implicit state (JNIEnv pointer)
_around_ the exception handler. The problem is that the function
'handle' has the type
handle :: (Exception -> IO a) -> IO a -> IO a
rather than
handle :: (Exception -> MonadIO a) -> MonadIO a -> MonadIO a

> revert to using an IORef, and use lexical scoping to define my
> callbacks in a location such that the reference to the environment is
> in scope.  This will work, but it's just not convenient to define all
> your functions inside another function so you can do a lexical scoping
> trick...

The stated motivation of the implicit configurations is precisely
that: make it appear that the IORef is `lexically scoped' over all of its
clients without putting all the clients inside one giant function.

The master file for the paper
http://www.eecs.harvard.edu/~ccshan/prepose/prepose.lhs
is a literate Haskell code, which you can load into GHCi as it is. You
can then run all of the examples in the paper.

If you have trouble using implicit configurations, have a particular
application in mind and can turn it into a self-contained example (by
replacing various functions with stubs wherever possible: e.g., see
the very end of prepose.lhs), you may want to let Ken and me
know. I'll see what can be done.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: Global Variables and IO initializers

[oleg]

Jo'n Fairbairn wrote:
> The idea is simply that we should provide a mechanism of
> saying to a compiler "this file (of data) is a module that
> exports only the variable v". ...
> So we tell the compilation system that file
> /somewhere/contains-v contains the value of the variable
> v::String, and that it lives in the imaginary module
> Home.Of.V, and when the resulting programme is loaded, so is
> the content of /somewhere/contains-v, and v is bound to it.

That seems to be similar to the following:

http://www.haskell.org/pipermail/haskell-cafe/2002-September/003423.html

In other words, we acknowledge the explicit phase separation and do the
initialization phase explicitly, and in Haskell. The advantage is that
the initialized variables look *exactly* as normal top-level variables
(and may be polymorphic). I believe Haskell plug-ins (reported at
Haskell Workshop 2004) is a far more advanced development and a
practical realization of the similar idea.

Incidentally, the above approach along with _many_ other approaches to
global variables are surveyed at
http://www.eecs.harvard.edu/~ccshan/prepose/prepose.pdf
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: Global Variables and IO initializers

[oleg]

Koen Claessen wrote:
> Imagine a commutative monad, CIO. Commutative monads have
> the property that it does not matter in what order actions
> are performed, they will have the same effect. In other
> words, for all m1 :: CIO A, m2 :: CIO B, k :: A -> B -> CIO
> C, it should hold that:
>
>   do a <- m1 do b <- m2
>  b <- m2 ===a <- m1
>  k a b  k a b

... provided 'a' and 'b' are distinct variables, right?

The following is legal in Haskell
> do
>   x <- ...
>   let foo = ... x ...
>   x <- ...
>   let foo = ... x ...

That shows that variables add a bit more complexity to the
question. Not only the dependency in actions should be considered, but
also data dependency. In the above code, if action 'm2' happens to
refer to the variable 'a', does commutativity still hold? Here are a
few more similar example, assuming the proposed 'global level <-'
syntax and the commutative nature of the action of creating an IORef:

> z <- newIORef x
> x = [y1,y2]
> y1 <- newIORef t
> y2 <- newIORef t
> t <- newIORef True

Should this be accepted? Should the actions be executed as written?
What if it were written
> y1 <- (return $! t) >>= newIORef

A similar example:

> class C a where op :: a -> a
> y <- newIORef (op (undefined::IORef Bool))
> x <- newIORef True
> instance C (IORef Bool) where op _ = x

which shows that the data dependency analysis is a bit trickier than
expected, even if the definitions appear to be `well-ordered'.

Template Haskell may bring some new complications. Suppose module A
imports module B and uses some of the functions of B at TH
time. Module A is also free to use bindings of B at run time. Now, if
module B has initializing actions, would they be executed once or
twice? Would created CIORefs be shared across the phases? Would that
behavior be consistent with respect to module A being compiled or
interpreted? These questions do arise in Scheme -- where the agreement
seems to be to have two kinds of imports: regular import and import
for-syntax. 

[regarding partial signatures]
> Ah! I had forgotten about that. See also:
>
>   http://www.mail-archive.com/[EMAIL PROTECTED]/msg05186.html

Incidently, some of that is already available in Haskell,
http://pobox.com/~oleg/ftp/Haskell/types.html#partial-sigs
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] How to close a type class

[oleg]

It is well known that type classes in Haskell are open. A user may at
any time extend a visible type class by providing a new
instance. There are situations where such an extensibility is
undesirable. We may want to prevent the user from adding an instance
to our class for some specific type -- or for all types (except some
finite set of types). This messages shows that this problem is
solvable in Haskell with common extensions. The code in this message
has been tested with GHC 6.2.1, GHC 6.3.20041106 snapshot, and Hugs
-98 (Nov 2003).

We first discuss the problem of excluding specific ground types from a
type class. That problem easily reduces to the one of defining a class
that has no instances and cannot have ones. We then describe excluding
non-ground types in the presence of overlapping (and perhaps,
incoherent) instance extensions. The latter solution shows how to
close a class -- that is, preclude adding any further instances to
it. Completely closing the class has a price to pay: the principal
type of an expression that involves closed class methods exists and
_can_ be inferred -- but cannot be explicitly written.

The essence of the technique can be expressed by a well-known phrase
How to replace failure by a [long...] list of successes

On Thu Nov 11 10:57:42 EST 2004 Ben Rudiak-Gould wrote on Haskell
Cafe:
> Except how would you prevent the user from declaring an instance for
> PrivateState RealWorld? Oh well. 

Let us indeed consider preventing the user from declaring an instance
of our class for a specific ground type. The answer is simple: we
declare that instance ourselves. But we make that instance
_statically_ unusable. Here's a simple example:

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module C1 where
>
> class C a where op:: a -> String
> instance C Int where op x  = show x
> instance C Char where op x = "char"

Suppose we wish to define two instances of that class, C Int and C
Char, and prevent the user from declaring an instance of C for a
string. So, we define that instance ourselves:

> instance Fail String => C String where op = error "thou shall not be"
>
> class Fail a
>
> test1 = op (1::Int)
> test2 = op 'z'
> --test3 = op "str"

Here class Fail has no instances (we shall discuss how to guarantee
that in a moment). If we uncomment out the test3 line, we get a type
error.

Thus we have reduced the problem of excluding certain types from a
typeclass to the problem of excluding all types from one particular
typeclass: Fail. How can we prevent the user from adding instances to
Fail? Again, we define the most general instance the class Fail may
have:

> instance Fail [a] => Fail a

If the test3 line stays commented out, the code typechecks and test1
and test2 work as expected. However, if we now uncomment the test3
line, we get the truly impressive type error message (I like the way
it looks in Hugs).

If overlapping instances extension is off, any attempt to add another
instance to class Fail will be rejected by the compiler, because it
will be overlapping with our general instance.


Let us now turn to a more complex problem of the exclusion of
non-ground types in the presence of overlapping instances. For
example, suppose we wish to prevent any instances of class C for
lists of any type. If overlapping instances are allowed, writing
instance Fail [a] => C [a] 
will not do us much good, because the user may still introduce 
"instance C [Int]" for specific ground types like Int.

Although overlapping (let alone incoherent) instance extensions seem
to be quite permissive, there is still a law they must obey: the law
of functional dependencies. That law lets us effectively close a
class. Indeed, functional dependencies are already a tool to
semi-close a class, to disallow a broad subset of instances (the ones
that fail the dependency).

Our solution requires adding a dummy type parameter to the type
class. Note that the signatures of class methods are not affected.

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-incoherent-instances #-}

We activate all extensions

> module C2 (C(..)) where
>
> data Private a -- NOT exported
>
> class C a b | a->b where op:: a -> String
> instance C Int (Private Int) where op x  = show x
> instance C Char (Private Char) where op x = "char"
> test1 = op (1::Int)
> test2 = op 'z'

Here we add a dummy class parameter 'b'. Note that the method
signature remains the same -- and so all the uses of the method.

To preclude the instantiation of the class for any list, we make the
instance ourselves:

> instance C [[a]] (Private [[a]])
> => C [a] (Private [a]) where op = error "thou shall not be"

The user may try to add a new instance, say
instance C [Int] ???
but what can he put instead of ??? Functional dependencies leave
*only* one choice: (Private [Int]) -- but the type constructor 

[Haskell] Re: Parameterized Show

[oleg]

George Russel wrote:
> Graham Klyne wrote (snipped):
>  > I like the principle of parameterizing Show to allow for different
>  > encoding environments...
>
> I like the idea too, not just for Show but for any instances.  It seems to
> me that in general you should be able to combine the convenience of the
> Haskell type system with the power of Standard ML's structures and functors.

That can be -- and has been -- done:
http://www.haskell.org/pipermail/haskell/2004-August/014463.html

The running example includes an ORD class -- which is like the Ord
class but can be parameterized by a comparison function, so to
speak. That is, there may be several ORD instances for one type --
e.g., several ways to compare integers. Also, we do not need to carry
the discriminating label or dictionary all the time. Here's a snippet
from the test in the above article:

> let set1_empty = inst fs LR (undefined::Int)
> s1  = add 1 (add 0 set1_empty)
> rm1  = member 2 s1

> set3_empty = inst fs LE (undefined::Int)
> s3  = add 1 (add 0 set3_empty)
> r3  = member 2 s3

we parameterize the applicative, translucent functor ORD->SET
with two different integer-comparison functions, represented by labels
LR and LE. More meaningful names are certainly possible. After we
instantiated the functor, we do not need to mention the ORD parameter
ever again. 

Ken Shan's paper, the above and the following messages
http://www.haskell.org/pipermail/haskell/2004-September/014515.html

argue that Haskell already has the full power of Standard ML's
structures and functors (and not only generative but applicative
functors as well).


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Closed Projections on HLists?

[oleg]

Jared Warren wrote:
> I'm doing some work with heterogeneous sets as provided by the HList
> library . My code uses
> projections of sets internally and I keep running into the open-world
> assumption when I ask the type checker to infer the result of
> projections. For example (in ghci):
>
> *> hProject hNil
> No instance for (HProject HNil l')
>
> ...When obviously the only valid projection from the empty set is the
> empty set.
>
> So what I'm wondering: is it possible to rewrite HProject in such a
> way as to allow the type checker to infer that the only possible
> projections from a list are its (non-proper) sublists?

If the inference is unique, then of course, we _can_ infer that the
empty list can only be projected onto the empty list. However any
non-empty list can be projected in several ways. How do we infer this
ambiguous result? Either we have to specify which projection result we
want, and the typechecker will tell us if that is possible. Or we
obtain the powerset of a list -- and then enumerate it. The current
HProject is written with the first approach in mind:

> class HProject l l'
>  where
>   hProject :: l -> l'

As we can see, there are no functional dependencies on the class -- as
there can't be, in general. A list can, in general, be projected in
many ways (and given a projection, there can be many lists it can be
obtained from). So, we have to be explicit: which list is to project
into what.

In general, that is the best one can do, right? There is however, a
special case: the empty list. The empty list can only be projected one
way -- and, so we would like the typechecker to infer that (rather
then wait for us to supply the result and then check it). If that
behavior is desirable, it can be obtained. The key is the ability to
specify functional dependencies on a per-instance basis.

Here's the complete code

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> -- Look, Ma! No overlapping instances!
>
> module Foo where
>
> import CommonMain hiding (HDeleteMany, hDeleteMany, TypeCast, 
>   typeCast, HProject, hProject)
> import TypeCastGeneric2
> import TypeEqTTypeable
> import TypeEqBoolTTypeable
> import TTypeable

> class HProject l l'
>  where
>   hProject :: l -> l'
>
> instance TypeCast HNil l' => HProject HNil l' where
>   hProject _ = typeCast HNil
> instance HProject (HCons a r) HNil
>  where
>   hProject l = HNil
> instance ( HList l', HOccurs' e (HCons a r), HProject (HCons a r) l')
>   => HProject (HCons a r) (HCons e l')
>  where
>   hProject l = HCons (hOccurs' l) (hProject l)
>
> list1 = (HCons 'a' (HCons True HNil))
>
>
> test1 = hProject list1 :: HNil
> test2 = hProject list1 :: (HCons Char HNil)
> test3 = hProject list1 :: (HCons Bool HNil)
>
> -- NB: No explicit type of the result given. The typechecker _does_
> -- infer it
> test4 = hProject HNil


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Typeful symbolic differentiation of compiled functions

[oleg]

Jacques Carette wrote on LtU on Wed, 11/24/2004

] One quick (cryptic) example: the same difficulties in being able to
] express partial evaluation in a typed setting occurs in a CAS
] [computer algebra system]. Of course I mean to have a partial
] evaluator written in a language X for language X, and have the partial
] evaluator 'never go wrong'.  Cheating by encoding language X as an
] algebraic datastructure in X is counter-productive as it entails huge
] amounts of useless reflection/ reification. One really wants to be
] able to deal with object-level terms simply and directly. But of
] course, that way lies the land of paradoxes (in set theory, type
] theory, logic)
]
] And while I am at it: consider symbolic differentiation. If I call
] that 'function' diff, and have things like diff(sin(x),x) == cos(x),
] what is the type of diff? More interestingly, what if I have D(\x ->
] sin(x) ) == \x -> cos(x) What is the type of D ? Is it implementable
] in Ocaml or Haskell?  [Answer: as far as I know, it is not.  But that
] is because as far as I can tell, D can't even exist in System F.  You
] can't have something like D operating on opaque lambda terms.]. But
] both Maple and Mathematica can. And I can write that in LISP or Scheme
] too.

In this message, we develop the `symbolic' differentiator for a subset
of Haskell functions (which covers arithmetics and a bit of
trigonometry). We can write

test1f x = x * x + fromInteger 1
test1 = test1f (2.0::Float)
test2f = diff_fn test1f
test2 = test2f (3.0::Float)

We can evaluate our functions _numerically_ -- and differentiate them
_symbolically_. Partial derivatives are supported as well. To answer
Jacques Carette's question: the type of the derivative operator (which
is just a regular function) is

  diff_fn :: (Num b, D b) => (forall a. D a => a -> a) -> b -> b

where the class D includes Floats. One can add exact reals and other
similar things. The key insight is that Haskell98 supports a sort of a
reflection -- or, to be precise, type-directed partial evaluation and
hence term reconstructions. The very types that are assumed of great
hindrance to computer algebra and reflective systems turn out
indispensable in being able to operate on even *compiled* terms
_symbolically_.

We must point out that we specifically do _not_ represent our terms as
algebraic datatypes. Our terms are regular Haskell terms, and can be
compiled! That is in stark contrast with Scheme, for example: although
Scheme may permit term reconstruction under notable restrictions, that
ability is not present in the compiled code. In general, we cannot
take a _compiled_ function Float->Float and compute its derivative
symbolically, yielding another Float->Float function. Incidentally,
R5RS does not guarantee the success of type-directed partial
evaluation even in the interpreted code.

Jacques Carette has mentioned `useless reflection/reification'. The
paper `Tag Elimination and Jones-Optimality' by Walid Taha, Henning
Makholm and John Hughes has introduced a novel tag elimination
analysis as a way to remove all interpretative overhead. In this
message, we do _not_ use that technique. We exploit a different idea,
whose roots can be traced back to Forth. It is remarkable how Haskell
allows that technique.

Other features of our approach are: an extensible differentiation rule
database; emulation of GADT with type classes.

This message is the complete code.

> {-# OPTIONS -fglasgow-exts #-}
> -- We only need existentials. In the rest, it is Haskell98!
> -- Tested with GHC 6.2.1 and 6.3.20041106-snapshot
>
> module Diff where
> import Prelude hiding ((+), (-), (*), (/), (^), sin, cos, fromInteger)
> import qualified Prelude

First we declare the domain of `differentiable' (by us) functions 

> class D a where
> (+):: a -> a -> a
> (*):: a -> a -> a
> (-):: a -> a -> a
> (/):: a -> a -> a
> (^):: a -> Int -> a
> sin:: a -> a
> cos:: a -> a
> fromInteger:: Integer -> a

and inject floats into that domain

> instance D Float where
> (+) = (Prelude.+)
> (-) = (Prelude.-)
> (*) = (Prelude.*)
> (/) = (Prelude./)
> (^) = (Prelude.^)
> sin = Prelude.sin
> cos = Prelude.cos
> fromInteger = Prelude.fromInteger


For symbolic manipulation, we need a representation for
(reconstructed) terms

> -- Here, reflect is the tag eliminator -- or `compiler'
> class Term t a | t -> a where
> reflect :: t -> a -> a

We should point out that the terms are fully typeful.

> newtype Const a = Const a deriving Show
> data Var a   = Var deriving Show
> data Add x y = Add x y deriving Show
> data Sub x y = Sub x y deriving Show
> data Mul x y = Mul x y deriving Show
> data Div x y = Div x y deriving Show
> data Pow x   = Pow x Int deriving Show
> newtype Sin x   = Sin x   deriving Show
> newtype Cos x   = Cos x   deriving Show


We can now describe the grammar of our term representation in the
following straightforward 

[Haskell] Re: A puzzle and an annoying feature

[oleg]

Andrew Bromage wrote:

> module FD where
>
> class C from to | from -> to where
>  g :: from -> to
>  h :: to -> from
>
> instance C Char Bool where
>  g c = c == 'T'
>  h b = if b then 'T' else 'F'
>
> --f :: (C Char a) => Char -> a
> f c = g c

Indeed, functional dependencies are the way to close a class that is
_visible_ to the typechecker (unlike the export directive that has no
such significance, at least to the inference algorithm).

The problem is that we wish to give 'f' a signature, like the one in
the commented code, but we cannot use the type variable 'a'. We must
use Bool -- which is silly as the typechecker would have figures it
out anyway.

> This is a pretty serious problem when you're doing typeclass
> metaprogramming.  In this case, the type you're trying to find is
> Bool.  In general, it might be a large complex type, generated by
> the class C as a typeclass metaprogram, which you don't want to put
> in the type signature for maintainability reasons.

Here's the way to solve the problem -- which is actually the problem
with the sequencing of FD resolution and other actions. The following
are the changes:


> instance (TypeCast Bool a, TypeCast a Bool) => C Char a where
>  g c = typeCast $ c == 'T'
>  h b = if (typeCast b) then 'T' else 'F'
>
> f :: (C Char a) => Char -> a
> f c =  g c
>
> -- snipped verbatim from the HList library
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x

The reason for TypeCast existence is to suitably delay the FD
resolution. TypeCast has permitted a lot of code that seemed
impossible.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] GADT and constraints [Was: Rebindable syntax for monads and arrows]

[oleg]

Simon Peyton-Jones wrote:

|[ data MyVec a where
|[   MkMyVec :: (Foo a) => a -> MyVec a
>
>   f x = case x of
>   MkMyVec x -> 
>
> constraints are always solved *lazily* when inferring, so we'd infer
> f :: Foo [a] => MyVec a -> ...
> even without any overlap
>
> but they are solved *eagerly* when checking against a
> user-supplied type sig
> so when checking
> f :: Eq a => MyVec a => ...
> we'd accept the program.  (If there were overlapping instances,
> we'd complain about them.)

I can't understand how constraints float at all. In the following code:

> class Foo1 a  where foo1 :: a -> String
> class Foo2 a  where foo2 :: a -> String
>
> instance Foo1 Bool where foo1 _ = "Bool"
> instance Foo2 Char where foo2 _ = "Char"
>
> data U a where
>   Ub :: a -> U a
>   Uc :: a -> U a
>
> foo (Ub a) = foo1 a
> foo (Uc a) = foo2 a

What is the type of foo? GHC snapshot 6.3.20041106 happily accepts
that code, and even infers 
*M> :t foo
foo :: forall a. (Foo2 a, Foo1 a) => U a -> String

but that seems odd. In any value of type U a, either Ub alternative is
present, or Uc. They can never be both. Then why do we get the
constraint that is the intersection of the two constraints rather than
the union of them?  BTW, when I tried to do

> data U a where
>   Ub :: Foo1 => a -> U a
>   Uc :: Foo2 => a -> U a


I received a message

> Couldn't match kind `*' against `k_a1QK -> *'
> In the class declaration for `Foo2'

which I found quite interesting. 

Anyway, even though GHC accepts the code and infers the type for foo,
the function is unusable. An attempt to evaluate 'foo (Ub True)' ends
up in an error message that there is no instance of Foo2 Bool. Indeed,
there isn't. But why that should matter if I'm only interested in the
Ub alternative? Again, the function 'foo' seems legitimate, and can be
easily expressed either in Martin Sulzmann's interpretation of GRDT
via existentials, or using the typeclass representation of GADT. For
example:

> data Ub a = Ub a
> data Uc a = Uc a
>
> class Foo t where foo:: t -> String
>
> instance Foo1 a => Foo (Ub a) where 
> foo (Ub a) = foo1 a
> instance Foo2 a => Foo (Uc a) where 
> foo (Uc a) = foo2 a

Here, the constraint Foo is clearly the `union' of Foo1 and Foo2 (the
discriminated union at that).

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: CFP: Continuation Fest 2008

[oleg]

Note: the Continuation Fest is scheduled on Apr 13, one day before FLOPS2008,
http://www.math.nagoya-u.ac.jp/~garrigue/FLOPS2008/
International Symposium on Functional and Logic Programming. Attendees
of the Continuation Fest who also participate in FLOPS have just
enough time get from Tokyo to Ise City in the morning of Apr 14; FLOPS
starts at 13:30. The detailed directions are available at
http://www.math.nagoya-u.ac.jp/~garrigue/FLOPS2008/access.html

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Continuation Fest 2008: Call for Participation

[oleg]

[Conrad Parker's presentation below will talk about continuations in Haskell]

Continuation Fest 2008: Call for Participation
http://logic.cs.tsukuba.ac.jp/Continuation/

Date: Sunday April 13, 2008.
Place: Akihabara-Daibiru Building, 13th Floor, Tokyo, Japan.
   (Akihabara Site of the University of Tokyo,
http://www.i.u-tokyo.ac.jp/map/index_e.shtml#aki)

Program (tentative):

13:00-13:05  Opening

Session 1. Demonstrating continuations
13:05-13:45  Kenichi Asai (Ochanomizu)
 Typing printf 
13:45-14:25  Oleg Kiselyov 
 Demo of persistent delimited continuations in OCaml
 for nested web transactions
(break)

Session 2. Applying continuations
14:35-15:05  Katsutoshi Itoh (Kahua project)
 Various use of continuations in Kahua
 - Application in practical web programming experience
15:05-15:35  Rui Otake (Tohoku)
 Delimited continuations in the grammar of Japanese
15:35-16:00  Conrad Parker (Kyoto)
 Continuations for video decoding and scrubbing
16:00-16:25  Takuo Watanabe (Titech) and Yuichi Tanaka 
 Continuing from the past: An approach to building
 dynamically upgradable applications
(break)

Session 3. Implementing continuations
16:35-17:15  Shinji Kono (Ryukyu)
 How to implement continuation only language in gcc 4.x
17:15-17:55  Koichi Sasada (Tokyo)
 Ruby Continuations

17:55-18:00  Closing

18:30-  Dinner

Participation:
No registration or participation fee is needed to attend
Continuation Fest except the dinner.
Those who join the dinner are encouraged to send an e-mail 
to the organizer by April 11th.

Program committee:
Chris Barker (New York), Shiro Kawai (Scheme Arts),
    Oleg Kiselyov (FNMOC), Chung-chieh Shan (Chair, Rutgers),
Taiichi Yuasa (Kyoto)

Organizers:
Kenichi Asai (Ochanomizu), Yukiyoshi Kameyama (Chair, Tsukuba),
Takahiro Kido (shelarcy)

Inquiries:
[EMAIL PROTECTED]
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] The initial view on typed sprintf and sscanf

[oleg]

We demonstrate typed sprintf and typed sscanf sharing the same
formatting specification. Our solution is surprisingly trivial: it
defines a simple embedded domain-specific language of formatting
patterns. The functions sprintf and sscanf are two interpreters of the
language, to build or parse a string according to the given
pattern. Our solution relies only on GADTs. We demonstrate that
lambda-abstractions at the type level are expressible already in the
Hindley-Milner type system; GADT with the included polymorphic
recursion help us use the abstractions.

The typed sprintf takes the formatting specification and several
arguments and returns the formatted string. The types and the number
of arguments depend on the formatting specification. Conversely, the
typed sscanf parses a string according to the formatting
specification, passing parsed data to a consumer function. Again, the
number and the types of the arguments to the consumer depend on the
formatting specification. The typed sprintf problem has been
investigated extensively: the first solution was shown by Danvy; more
solutions were proposed by Hinze and Asai. The typed scanf problem
received significantly less attention, if any. It seems that the
implementation of the typed sprintf and sscanf sharing the same
formatting specification has not been known.

Here are a few examples of the typed sprintf and sscanf

> tp1 = sprintf $ lit "Hello world"
> -- "Hello world"
> ts1 = sscanf "Hello world" (lit "Hello world")  ()
> -- Just ()

> tp2 = sprintf (lit "Hello " ^ lit "world" ^ char) '!'
> -- "Hello world!"
> ts2 = sscanf "Hello world!" (lit "Hello " ^ lit "world" ^ char) id
> -- Just '!'

> fmt3 = lit "The value of " ^ char ^ lit " is " ^ int
> tp3 = sprintf fmt3 'x' 3
> -- "The value of x is 3"
> ts3 = sscanf "The value of x is 3" fmt3 (\c i -> (c,i))
> -- Just ('x',3)

A formatting specification is built by connecting primitive
specifications (such as lit "string", int, char) with (^). We observe
that whereas 
 sprintf $ lit "Hello world"
has the type String, 
 sprintf $ lit "The value of " ^ char ^ lit " is " ^ int
has the type Char -> Int -> String. Likewise, the type of the consumer
of the values parsed by sscanf varies with the formatting specification.
The example of tp3 and ts3 demonstrates that sprintf and sscanf can
indeed use exactly the same formatting specification, which
is a first-class value.

Printf and scanf are present in many languages (e.g., C and Haskell);
in most of the cases, they are not type-safe: the type checker does
not stop the programmer from passing to printf more or fewer arguments
than required by the formatting string. OCaml supports typed sprintf
and sscanf, which relies on a particular weird typing of these
functions, resulting in formatting specifications being not first
class. Our sscanf has exactly the same interface as that in OCaml,
modulo weird typing.

The complete code of the typed sprintf and sscanf with more examples
is available at
http://okmij.org/ftp/Haskell/PrintScan.hs
It can be used in Haskell programs as it is; it is trivial to arrange
it in a Haskell library or Hackage package.


Our implementation is based on the observation of Hinze (Ralf
Hinze. Functional Pearl: Formatting: a class act. JFP, 13(5):935-944,
September 2003) that the formatting specification is a `type
transformer', a functor. For example, the formatting specification
'int' is associated with a functor transforming a type 't' to a type
'Int -> t'. Hinze represented functors in Curry style; the
functor associated with 'int' is then (Int ->).  However, a more
direct, Church-style representation is also possible.  Let us consider
a type "F a b" where "F" is a binary type constructor, "a" is a type
variable, and "b" is a type that may include one or more occurrences of
"a". That type is essentially a type abstraction, the type-level
lambda-function. To apply the function to an argument, we unify "a"
with the argument; the second parameter of "F" is the result of the
application. This is the standard emulation of lambda-calculus in
Prolog.

Based on this observation, we define the language of formatting
specifications as follows:

> data F a b where
> FLit :: String -> F a a
> FInt :: F a (Int -> a)
> FChr :: F a (Char -> a)
> (:^) :: F b c -> F a b -> F a c

> (^)  = (:^)
> lit  = FLit
> int  = FInt

The type of (:^) expresses the inverse functional composition of two
type-level lambdas; one may read "F" as `big lambda'.

The formatting specification can be interpreted in two different ways,
for printing and for parsing. The types of the interpreters are pleasingly
symmetric:

> intp :: F a b -> (String -> a) -> b
> intp (FLit str) k = k str
> intp FChr   k = \x -> k [x]
> intp (a :^ b)   k = intp a (\sa -> intp b (\sb -> k (sa ++ sb)))


> ints :: F a b -> String -> b -> Maybe (a,String)
> ints (FLit str) inp x = maybe Nothing (\inp' -> Just (x,inp')) $ 
>   prefix str inp

[Haskell] The final view on typed sprintf and sscanf

[oleg]

It would be remiss not to mention the dual solution to the problem of
typed sprintf and sscanf sharing the same formatting
specification. The previous message defined the embedded
domain-specific language of formatting specifications in the initial
style, as a data type. The language can also be defined in the final
style. To the end user, the difference is hardly noticeable: all the
tests of the previous message work as they are (modulo a few
adjustments caused by the monomorphism restriction). However, whereas
the initial style required GADT, the final solution is entirely in
Haskell98. One often hears that hardly anything interesting can be
written in Haskell98. I submit that implementing type-indexed terms,
thought to require GADTs or similar dependent-type-like extensions,
ought to count as interesting.

Again, the formulation of the problem and the end-user interface
remain exactly the same as described in the previous message. Here are
a few examples:

> tp1 = sprintf $ lit "Hello world"
> -- "Hello world"
> ts1 = sscanf "Hello world" (lit "Hello world")  ()
> -- Just ()

> tp2 = sprintf (lit "Hello " ^ lit "world" ^ char) '!'
> -- "Hello world!"
> ts2 = sscanf "Hello world!" (lit "Hello " ^ lit "world" ^ char) id
> -- Just '!'

> fmt3 () = lit "The value of " ^ char ^ lit " is " ^ int
> tp3 = sprintf (fmt3 ()) 'x' 3
> -- "The value of x is 3"
> ts3 = sscanf "The value of x is 3" (fmt3 ()) (\c i -> (c,i))
> -- Just ('x',3)

The only difference is the dummy unit argument to the fmt3
term, to keep it polymorphic and away from the monomorphism
restrictions. Otherwise, the examples look the same and work the same.
The complete code is available at
http://okmij.org/ftp/Haskell/PrintScanF.hs
It is Haskell98 and should work on any Haskell98 system (tested on GHC
6.8.2 and Hugs September 2006).

Whereas the initial version defined the formatting language with the
help of GADT, the final version uses a simple, single-parameter type
class

> class FormattingSpec repr where
> lit  :: String -> repr a a
> int  :: repr a (Int -> a)
> char :: repr a (Char -> a)
> (^)  :: repr b c -> repr a b -> repr a c
> infixl 5 ^

The printer and the scanner are two interpreters of the language

> newtype FPr a b = FPr ((String -> a) -> b)
> instance FormattingSpec FPr where
> lit str = FPr $ \k -> k str
> char= FPr $ \k -> \x -> k [x]
> (FPr a) ^ (FPr b)  = FPr $ \k -> a (\sa -> b (\sb -> k (sa ++ sb)))

> newtype FSc a b = FSc (String -> b -> Maybe (a,String))
> instance FormattingSpec FSc where
> lit str = FSc $ \inp x -> 
> maybe Nothing (\inp' -> Just (x,inp')) $ prefix str inp
> char= FSc $ \inp f -> case inp of
>(c:inp)  -> Just (f c,inp)
>""   -> Nothing
> (FSc a) ^ (FSc b) = FSc $ \inp f ->
> maybe Nothing (\(vb,inp') -> b inp' vb) $ a inp f

> sprintf :: FPr String b -> b
> sprintf (FPr fmt) = fmt id
> sscanf :: String -> FSc a b -> b -> Maybe a
> sscanf inp (FSc fmt) f = maybe Nothing (Just . fst) $ fmt inp f

The transformation from the initial to the final style follows the
correspondence described in
http://okmij.org/ftp/Computation/tagless-typed.html#in-fin
In fact, PrintScanF.hs was `derived' from PrintScan.hs by Emacs `code
movements'. Once the syntax errors have been fixed, the code
worked on the first try.

One can easily define a yet another interpreter, to convert the
formatting specification to a C-like format string.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] type inference & instance extensions

[oleg]

Doug McIlroy wrote:
> A fragment of an attempt to make pairs serve as complex numbers,
> using ghc/hugs extensions:
>
> instance Num a => Num (a,a) where
> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>
> Unfortunately, type inference isn't strong enough to cope with
>
> (1,1)*(1,1)

It is not quite difficult to tell the type checker that if pairs of
numbers are numbers, the two components of the pair must have the same
type. We say so literally. We first should make the instance more
general to permit any pair, of the type (a,b) to match. We next impose
the constraint that the types a and b must be in the class Num;
furthermore, the types a and b must be the same. Here is the complete
solution that should work on GHC 6.4, 6.6, 6.8, and probably of
earlier and later versions.
 
> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
>   UndecidableInstances, FlexibleInstances #-}
>
> module D where
>
> instance (Num a, Num b, TypeCast b a, TypeCast a b) => Num (a,b) where
> (x,y) * (u,v) = (typeCast x * typeCast u - typeCast y * typeCast v, 
>  typeCast x * typeCast v + typeCast y * typeCast u)
> (x,y) + (u,v) = (typeCast x + typeCast u, 
>  typeCast y + typeCast v)
> (x,y) - (u,v) = (typeCast x - typeCast u, 
>  typeCast y - typeCast v)
> fromInteger x = (fromInteger x, 0)
>
> test1 = (1,1) * (2,2)-- (0.0,4.0)
> test2 = (1.1,1) * (2,2)  -- (0.20018,4.2)
> test3 = test1 * test2-- (-16.8,0.8007)
> test4 = (test1 + test3) * (test1 - test3) -- (-297.6,26.8800024)
> test4' = -16 - test3 * test3 -- (-297.6,26.8800024)
>
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x

As one can see, we added typeCast before every variable, indicating
that an application of the equality constraint is needed. We let the GHC
figure out what should be `cast' to what.

The recent versions of GHC have a nifty equality constraint, so the
code can be written simply

> {-# LANGUAGE TypeFamilies #-}
>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module D where
>
> instance (Num a, Num b, a ~ b) => Num (a,b) where
> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
> 
> test1 = (1,1) * (2,2)

It does typecheck in GHC 6.8.2; alas, running the code produces

> ghc-6.8.2: panic! (the 'impossible' happened)
>   (GHC version 6.8.2 for i386-unknown-freebsd):
>   nameModule $dNum{v aJiF}

I guess one needs to upgrade to GHC 6.10. The solution using TypeCast,
however inelegant, works on GHC 6.8 and earlier compilers.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Lazy IO breaks purity

[oleg]

We demonstrate how lazy IO breaks referential transparency.  A pure
function of the type Int->Int->Int gives different integers depending
on the order of evaluation of its arguments. Our Haskell98 code uses
nothing but the standard input.  We conclude that extolling the purity
of Haskell and advertising lazy IO is inconsistent.

Henning Thielemann wrote on Haskell-Cafe:
> Say I have a chain of functions: read a file, ... write that to a file,
> all of these functions are written in a lazy way, which is currently
> considered good style

Lazy IO should not be considered good style. One of the common
definitions of purity is that pure expressions should evaluate to the
same results regardless of evaluation order, or that equals can be
substituted for equals. If an expression of the type Int evaluates to
1, we should be able to replace every occurrence of the expression with
1 without changing the results and other observables. 

The expression (read s) where s is the result of the (hGetContents h1)
action has the pure type, e.g., Int. Yet its evaluation does more than
just producing an integer: it may also close a file associated with
the handle h1. Closing the file has an observable effect: the file
descriptor, which is a scarce resource, is freed. Some OS lock the
open file, or prevent operations such as renaming and deletion on the
open file. A file system whose file is open cannot be
unmounted. Suppose I use an Haskell application such as an editor to
process data from a removable drive. I mount the drive, tell the
application the file name. The (still running) application finished
with the file and displayed the result. And yet I can't unplug the
removable drive, because it turns out that the final result was
produced without needing to read all the data from the file, and the
file remains unclosed.

Some people say: the programmer should have used seq. That is the
admission of guilt! An expression (read s)::Int that evaluates to 1 is 
equal to 1. So, one should be able substitute (read s) with 1. If the
result of evaluating 1 turns out not needed for the final outcome,
then not evaluating (read s) should not affect the outcome. And yet it
does. One uses seq to force evaluation of an expression even if the
result may be unused. Thus the expression of a pure type 
has *side-effect*. 

The advice about using seq reminds me of advice given to C programmers
that they should not free a malloc'ed pointer twice, dereference a
zero pointer and write past the boundary of an array. If lazy IO is
considered good style given the proper use of seq, then C should be
considered safe given the proper use of pointers and arrays.

Side affects like closing a file are observable in the external
world. A program may observe these effects, in an IO monad. One can
argue there are no guarantees at all about what happens in the IO
monad. Can side-effects of lazy IO be observable in _pure_ Haskell
code, in functions with pure type? Yes, they can. The examples are
depressingly easy to write, once one realizes that reading does have
side effects, POSIX provides for file descriptor aliasing, and sharing
becomes observable with side effects. Here is a simple Haskell98 code.


> {- Haskell98! -}
>
> module Main where
>
> import System.IO
> import System.Posix.IO (fdToHandle, stdInput)
>
> -- f1 and f2 are both pure functions, with the pure type.
> -- Both compute the result of the subtraction e1 - e2.
> -- The only difference between them is the sequence of
> -- evaluating their arguments, e1 `seq` e2 vs. e2 `seq` e1
> -- For really pure functions, that difference should not be observable
>
> f1, f2:: Int -> Int -> Int
>
> f1 e1 e2 = e1 `seq` e2 `seq` e1 - e2
> f2 e1 e2 = e2 `seq` e1 `seq` e1 - e2
>
> read_int s = read . head . words $ s
>
> main = do
>let h1 = stdin
>h2 <- fdToHandle stdInput
>s1 <- hGetContents h1
>s2 <- hGetContents h2
>print $ f1 (read_int s1) (read_int s2)
>-- print $ f2 (read_int s1) (read_int s2)


One can compile it with GHC (I used 6.8.2, with and without -O2) and
run like this
   ~> /tmp/a.out 
   1
   2
   -1
That is, we run the program and type 1 and 2 as the inputs. The
program prints out the result, -1. If we comment out the line
"print $ f1 (read_int s1) (read_int s2)" and uncomment out the last
line the transcript looks like this
   ~> /tmp/a.out 
   1
   2
   1

Running the code with Hugs exhibits the same behavior. Thus a pure
function (-) of the pure type gives different results depending on the
order of evaluating its arguments.

Is 1 = -1?






___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Definitions of purity and Lazy IO

[oleg]

As Amr Sabry aptly observed more than a decade ago discussions of
purity and referential transparency usually lead to confusion and
disagreement. His JFP paper provided the needed rigor and argued that
Haskell even _with regular file (stream) IO_ is pure. As was shown
yesterday, with Lazy IO, Haskell is not pure.

Before we discuss definitions, let us note the motivations. Suppose I
have a Haskell program. As every single (compiled) Haskell program it
has the main function, of the type IO a for some a. It must use IO, at
least to print the final result, the observation of the
program. Suppose the program contains the expression "e1 + e2" adding
two integer expressions. Can I replace this expression with "e2 + e1"
and be sure the observations of my program are unaffected?

If one says that ``you should assume that every IO operation returns a
random result''  then we have no ability to reason about any
real Haskell program. We can't be sure of soundness of any compiler
optimization. So, Haskell is far worse than C!? With C, Xavier Leroy
has managed to create a provably correct optimizing compiler, and
mechanically _prove_ the soundness of all optimizations. A C program,
just like a Haskell program, must use IO at least to print the
final result. We can never hope to build a provably correct compiler for
Haskell? We cannot prove observational equivalences of any real
Haskell program? Isn't that sad?

The formal question is thus: are the following two expressions f1 and f2,
of a *pure type* Int->Int->Int 

f1, f2:: Int -> Int -> Int
f1 = \e1 e2 -> case (e1,e2) of
(1,_) -> e1 - e2
(_,_) -> e1 - e2

f2 = \e1 e2 -> case (e1,e2) of
(_,1) -> e1 - e2
(_,_) -> e1 - e2

equal? Before one invokes an equational theory or says that both these
expressions are just integer subtraction, let me clarify the
question: are f1 and f2 at least weakly observationally equivalent?
That is, for any program context C[] such that C[f1] is well-typed, 
the program C[f2] must too be well-typed, and if one can observe the
result of C[f1] and of C[f2], the two observations must be identical. The
observation of a program may (and often does) involve side-effects and
IO (more on it below). The message posted yesterday exhibited a context C[] that
distinguishes f1 from f2. Thus, in presence of Lazy IO, any equational
theory that equates f1 and f2 cannot be sound. I don't think one can
design such a context C[] using the regular, eager file IO.

Amr Sabry in a paper ``What is a Purely Functional Language?''
J. Functional Programming, 8(1), 1-22, Jan. 1998. 
http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps

proposed the definition of purity, see p 2 and Definition 4.7. The
definition essentially states that call-by-name, call-by-value and
call-by-need evaluation functions must be weakly equivalent. These
evaluation functions map programs to observables. The part of
evaluation dealing with observing the answers may have side effects!
Sec 5.1 rigorously shows that lambda-calculus with global state
and destructive mutation may be called pure functional, if
effects are regarded as values and the program is written in what we
now call a monadic style (whose idea was proposed by Reynolds back in
1981 when studying Idealized Algol). The end of Sec 5.1 remarks that
IO can be treated that way -- and in fact, Appendix D of Haskell
report 1.2 indeed had described such a semantics of IO:
http://haskell.org/definition/haskell-report-1.2.ps.gz
(the appendix starts on p. 139). Thanks to Paul Hudak for pointing this
out three years ago.

Thus Haskell even with IO may be called pure functional. With Lazy IO,
it can no longer be called pure functional as different orders of
evaluation of arguments of a function lead to different program
observations.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: indirectly recursive dictionaries

[oleg]

Ralf wrote:
> class C1 x
>  where
>  m1 :: x -> ()
>  m1 = const undefined

> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x

> class C2 x y | x -> y
> instance C2 Int Int

> bar :: ()
> bar = m1 (1::Int)

I believe it works very well (meaning bar typechecks and even runs)
if we either add an instance 
instance C1 Int
or change the instance of C2 to
instance C2 Int Bool
Otherwise, the problem really has no solution, and looping is an
indication. I used GHC 6.8.3
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: indirectly recursive dictionaries

[oleg]

Tom Schrijvers wrote:
> The cyclic dictionaries approach is a bit fragile. The problem appears to
> be here that GHC alternates exhaustive phases of constraint reduction and
> functional dependency improvement. The problem is that in your example you
> need both for detecting a cycle.

It seems we can convince GHC to do constraint reduction and
improvement in the order we desire. The key is to use the
continuation-passing style -- which forces things to happen in the
right order, both at the run-time and at the compile time. I took the
liberty to flesh out the example a bit more, to verify that recursive
dictionaries are indeed constructed and used. The trace statement
shows it.

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}

import Debug.Trace

class C1 x where
 m1 :: x -> Int

instance (C1 x, C1 y) => C1 (x,y) where 
m1 (x,y) = m1 x + m1 y
instance C1 Bool where 
m1 = fromEnum
-- Was: instance (C2 x y, C1 (y,Bool)) => C1 x
instance C2CPS x (C1K Bool) => C1 x where
m1 x = trace "recursive C1" $ c2invoke (C1K True) x

newtype C1K a = C1K a

-- The class C2CPS below is a CPS version of the class C2 below
-- class C2 x y | x -> y where c2 :: x -> y
-- instance C2 Int Int where c2 = id
-- The functional dependency becomes implicit

class C2CPS x k where
c2invoke :: k -> x -> Int
instance Apply k Int Int => C2CPS Int k where
c2invoke k x = apply k x

class Apply f x y | f x -> y where
apply:: f -> x -> y
instance C1 (b,a) => Apply (C1K a) b Int where
apply (C1K a) x = m1 (x,a)

-- It is this declaration that was causing nontermination of typechecking.
-- Not any more
bar :: Int
bar = m1 (1::Int)

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Safe and generic printf with C-like format string

[oleg]

The familiar printf is unsafe: nothing prevents us from passing to
printf more or fewer arguments than required by the format
specification, or passing the arguments of wrong types. The error is
discovered only at run-time. The implementation of printf in Haskell,
alas, retains this problem. There is also a desire to better integrate
printf with Show, so we can format the value of any showable type:
we'd like to have something like the ~a specification of Common Lisp.

Integrating printf with show, thus making it generic, is quite
easy. The implementation is still Haskell98. It has just been posted:

http://www.haskell.org/pipermail/haskell-cafe/2009-June/062410.html

Given its simplicity, one may wonder why it was not mentioned in the
Haskell98 report or included in standard libraries. The safety problem
still remains: we'd like to prevent the mismatch between
the arguments of printf and the format specification statically. That
too is easy to accomplish. Type-safe printf has been described by
Olivier Danvy back in 1998. It is part of SML/NJ. The only remaining
bit is to convert the formatting _string_ to the more representative
and more useful to the type-checker form. That too is easy, with
Template Haskell (as Ryan Ingram remarked).

The following code implements that suggestion. Aside from the use of
template Haskell, it is Haskell98. Beside the familiar format
specifications %s and %d, in implements the specification %a to
format any showable value. The code is available at
http://okmij.org/ftp/typed-formatting/TotalPrintF.hs
http://okmij.org/ftp/typed-formatting/TFTest.hs

The second file contains these examples:

module TFTest where

import TotalPrintF

t1 = printf $(spec "Hello, there!")
-- "Hello, there!"

t2 = printf $(spec "Hello, %s!") "there"
-- "Hello, there!"

t3 = printf $(spec "The value of %s is %d") "x" 3
-- "The value of x is 3"

-- Mismatch between the formatting string and the printf arguments
-- is a type error.

-- t31 = printf $(spec "The value of %s is %d") "x" True
-- Couldn't match expected type `Bool' against inferred type `Int'

{-
t32 = printf $(spec "The value of %s is %d") "x" 3 10
Couldn't match expected type `t1 -> t'
   against inferred type `String'
Probable cause: `printf' is applied to too many arguments
-}

t4 = let x = [9,16,25] 
 i = 2 
 in printf $(spec "The element number %d of %a is %a") i x (x !! i)
-- "The element number 2 of [9,16,25] is 25"



___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Three new implementations of multi-prompt delimited control

[oleg]

The monadic framework for delimited continuations described in
the paper by Dybvig, Peyton Jones and Sabry (JFP 2007) has found
many applications, for example, fair backtracking search, final
zippers, direct-style web programming, direct-style code generation,
and probabilistic programming. The extensive experience suggested
improvements in efficiency and, mainly, programmer's convenience. The
three new libraries are novel implementations of the enhanced
framework. Prompts, for instance, can now be bound to top-level
identifiers and do not have to be passed around explicitly or through
the extra Reader monad.  The new libraries benefited from the
experience of implementing delimited control on several platforms.

All three libraries provide monad transformers, with basic operations
to capture and reinstall delimited continuations: pushPrompt, shift,
shift0, control, takeSubCont/pushSubCont.  All three libraries support
multiple, typed prompts. All three libraries are quite distinct from
the original implementation in Dybvig, Peyton Jones, Sabry's
paper. For instance, none of the new libraries use unsafeCoerce.  All
three implementations are derived from the specification of delimited
control: from the reduction semantics or from the definitional
interpreter.

The new libraries differ in
  -- performance
  -- ease of understanding
  -- constraints on the base monad or the prompt types
  -- flavors of prompts and support for global prompts

The libraries are named CCRef, CCExc and CCCxe. The complete code
of the libraries along with the regression test suite are publicly
available at
http://okmij.org/ftp/continuations/CCmonad/
The directory includes sample code (Generator1.hs and Generator2.hs),
implementing generators like those of Python. A more extensive
example is the porting of the LogicT library (of fair backtracking
monad transformers), from the old CC implementation to CCExc/CCCxe:
http://okmij.org/ftp/Haskell/LogicT.tar.gz
One of the sample applications of LogicT, of a computer playing 
5x5 tic-tac-toe against itself, was used as a macro-benchmark of the
libraries. The end of the file TicTacToe.hs summarizes the results.
The new libraries are faster (so the reader who may wish to play 
will have less time to think).


The library CCRef is closest to the interface of Dybvig, Peyton Jones
and Sabry. CCRef is derived from the definitional interpreter using the
implementation techniques described and justified in the FLOPS 2010
paper. The monad transformer CC implemented by CCRef requires the base
monad to support reference cells. In other words, the base monad must
be a member of the type class Mutable: that is, must be IO, ST, STM or
their transformer. CCRef adds to the original interface the frequently
used function abortP as a primitive.

As one may notice from their names, the libraries CCExc and CCCxe are
closely related. CCCxe is derived as a CPS version of CCExc.  CCCxe is
sometimes more efficient; it is always less perspicuous. Both
libraries provide the identical interface and are interchangeable. It
seems that CCExc is faster at delimited control but imposes more
overhead on the conventional code; CCCxe is dual. It pays to use CCCxe
in code with long stretches of determinism punctuated by fits and
restarts.

We now explain new features of CCExc. It is the most direct
implementation of the bubble-up (bottom-up) reduction semantics of
multi-prompt delimited control, described on
PDF page 57 of http://okmij.org/ftp/gengo/CAG-talk.pdf

Unlike all other implementations of delimited control in Haskell,
CCExc is _not_ based on the continuation monad. Rather, the monad of
CCExc is an extension of the Error monad: a monad for restartable
exceptions. CCExc offers not one monad transformer but a family (CC
p), parameterized by the prompt flavor p. The library defines several
prompt flavors; the users are welcome to define their own.

Prompt flavors are inherently like exception flavors (the FLOPS 2010
paper even calls prompts `exception types' or `exception envelopes').
Control.Exception defines singular global exceptions such as
BlockedOnDeadMVar.  There are global exceptions like ErrorCall,
parameterized by the error string. There are closed global variants,
such as ArithException, with the fixed number of alternatives. There
are also open variants, SomeException, with any number of potential
alternatives. Users may define their own exception types, whose
visibility may be restricted to a module or a package. Finally, one
may even generate distinct expression types dynamically, although that
is seldom needed.

The libraries CCExc and CCCxe support all these flavors. On one end is
the prompt flavor (PS w). There is only one prompt of that flavor,
which is globally defined and does not have to be passed around.  The
monad transformer (CC (PS w)) then is the monad transformer for
regular, single-prompt delimited continuations, for the answer-type w.
Danvy/Filinski test, which looks in Sc