https://wiki.haskell.org/api.php?action=feedcontributions&user=Robdockins&feedformat=atomHaskellWiki - User contributions [en]2021-05-18T12:27:48ZUser contributionsMediaWiki 1.27.4https://wiki.haskell.org/index.php?title=Type_SK&diff=5331Type SK2006-08-11T12:47:36Z<p>Robdockins: </p>
<hr />
<div>Subject: [Haskell] The GHC typechecker is Turing-complete<br/><br />
Date: August 10, 2006 10:04:23 PM EDT<br />
<br />
This message is literate Haskell so you can all follow along at home.<br />
The program developed in this message was tested on GHC 6.4.2.<br />
<br />
My purpose today is to show that the GHC typechecker with multi-parameter<br />
typeclasses, functional dependencies, and undecidable instances is Turing-<br />
complete. Some time ago on this mailing list, there was a brief discussion<br />
about a lambda calculus and a direct Turing-machine implementation; either <br />
would be sufficient to demonstrate the Turing-completeness of the typechecker.<br />
However, neither implementation was preserved on-list, and the links are<br />
now dead.<br />
<br />
''Note: I have since been informed of the [http://www.lochan.org/keith/publications/undec.html current home of the TM implementation].''<br />
<br />
My strategy will be to embed the SK combinator calculus. The SK combinator<br />
calculus is capable of embedding the lambda calculus, which is well-known<br />
to be Turing-complete. Furthermore, the SK calculus is simpler to implement<br />
than the lambda calculus.<br />
<br />
For a complete proof of Turing-completeness, one should have a correctness<br />
proof for the embedding. I do not undertake such a proof here, but I will<br />
demonstrate what I hope to be convincing evidence for the correctness of<br />
this embedding.<br />
<br />
<br />
I begin by throwing the switches that give me the needed extensions.<br />
<br />
> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}<br />
> module SK where<br />
<br />
Next I define the terms of the SK combinator basis. This includes symbols for<br />
the combinators themselves, a symbol for application, and a way to introduce<br />
arbitrary uninterpreted types into computations.<br />
<br />
> data K0 <br />
> data S0<br />
> data App x y<br />
> data Other a<br />
<br />
Now I proceed to create the evaluator by first defining a single-step reduction<br />
relation. This relation is carefully designed to be reflexive on normal forms,<br />
and always reduces the leftmost-outermost redex. I then form the final<br />
evaluation relation by taking the transitive closure of single-step reduction.<br />
<br />
The semantics of typeclass constraint satisfaction are basicly strict. That<br />
is, the typechecker will make sure to fully evaluate all class constraints<br />
and fully instantiate all types whether or not those types turn out to be<br />
needed. Because of this, I need to be careful to form the transitive closure<br />
in a way that doesn't cause the typechecker to diverge on evaluation when it<br />
should not (of course, the typecheker will diverge on divergent terms).<br />
<br />
In order to do this, I define the single-step reduction relation so that it<br />
returns an additional result in addition to the reduced term. This result<br />
indicates 'More' whenever a redex was found and reduced and 'Done' otherwise.<br />
<br />
A few reduction rules perform reduction in parallel. These rules will return<br />
'More' if reduction was performed on any subterm.<br />
<br />
> data Done<br />
> data More<br />
<br />
> class CombineDone d1 d2 d | d1 d2 -> d<br />
> instance CombineDone Done Done Done<br />
> instance CombineDone Done More More<br />
> instance CombineDone More Done More<br />
> instance CombineDone More More More<br />
<br />
<br />
The 'Eval1' relation performs a single step of reduction. The presentation<br />
of this relation is somewhat tedious because we are forced to enumerate each<br />
possible spine shape up to 4 'App's deep. I could possibly do this more<br />
concisely if I enabled overlapping instances.<br />
<br />
> class Eval1 x y d | x -> y d<br />
<br />
I start by providing axioms stating that atomic terms evaluate to themselves<br />
with no reduction.<br />
<br />
> instance Eval1 S0 S0 Done<br />
> instance Eval1 K0 K0 Done<br />
> instance Eval1 (Other a) (Other a) Done<br />
<br />
There are a number of cases which just propagate evaluation contexts underneath<br />
the right-hand side of of 'App' when the spine shape cannot be reduced any<br />
further. These fairly uninteresting cases are collected together here.<br />
<br />
> instance Eval1 x x' d => Eval1 (App K0 x) (App K0 x') d<br />
> instance Eval1 x x' d => Eval1 (App S0 x) (App S0 x') d<br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , CombineDone d1 d2 d<br />
> ) => Eval1 (App (App S0 x) y) (App (App S0 x') y') d<br />
><br />
> instance Eval1 x x' d => Eval1 (App (Other a) x) (App (Other a) x') d<br />
> <br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , CombineDone d1 d2 d<br />
> ) => Eval1 (App (App (Other a) x ) y )<br />
> (App (App (Other a) x') y') d<br />
><br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , Eval1 z z' d3<br />
> , CombineDone d1 d2 d4<br />
> , CombineDone d3 d4 d<br />
> ) => Eval1 (App (App (App (Other a) x ) y ) z )<br />
> (App (App (App (Other a) x') y') z') d<br />
<br />
Now we get to the real meat. Here are the rules for reducing the 'K'<br />
combinator. There are rules for reducing under both 2 and 3 'App's.<br />
<br />
> instance Eval1 (App (App K0 x) y) x More<br />
> instance Eval1 (App (App (App K0 x) y) z) (App x z) More<br />
<br />
And here, the rule for reducing the 'S' combinator.<br />
<br />
> instance Eval1 <br />
> (App (App (App S0 f) g) x)<br />
> (App (App f x) (App g x))<br />
> More<br />
<br />
Finally, a rule to decompose an arbitrary 'App' context. I propagate<br />
the evaluation context down the left side of an 'App' only when that<br />
'App' is not involved in any redexes. This implements the leftmost-<br />
outermost strategy. In any leftmost spine consisting of 4 'App's,<br />
the leftmost 'App' can never be involved in any redex. The cases for<br />
other levels of 'App's are folded into the above rules.<br />
<br />
> instance ( Eval1 (App (App (App p q) x) y) a d<br />
> ) => Eval1 (App (App (App (App p q) x) y) z) (App a z) d<br />
<br />
<br />
Now I need to take the transitive closure of the 'Eval1' relation. I do<br />
this with the auxiliary 'EvalAux' class. The first instance represents<br />
the base case, where 'Eval1' performed no reductions. The second instance<br />
implements the transitivity and does bookkeeping with the termination markers.<br />
<br />
> class EvalAux x y q1 | x q1 -> y<br />
><br />
> instance EvalAux x x Done<br />
><br />
> instance ( Eval1 x y q<br />
> , EvalAux y z q<br />
> ) => EvalAux x z More<br />
<br />
<br />
Now at last I can define the evaluation relation. It is defined in terms of<br />
'EvalAux' and hides the termination bookkeeping.<br />
<br />
> class Eval x y | x -> y<br />
> instance EvalAux x y More => Eval x y<br />
<br />
<br />
I define convenient functions to allow me to invoke the type evaluators<br />
and a synonym for 'undefined' to cut down on typing.<br />
<br />
> eval1 :: Eval1 x y q => x -> y<br />
> eval1 = undefined<br />
<br />
> eval :: Eval x y => x -> y<br />
> eval = undefined<br />
<br />
> bot :: a<br />
> bot = undefined<br />
<br />
Before showing off the evaluator, I'm going to need several dummy types<br />
to work with.<br />
<br />
> data P0<br />
> data Q0<br />
> data R0<br />
<br />
> type P = Other P0<br />
> type Q = Other Q0<br />
> type R = Other R0<br />
<br />
Now, some examples of the SK evaluator in action. First I show<br />
that the S and K combinators have their expected axiomatic behavior.<br />
(Note, the following demonstrations rely on definitions found in the<br />
appendix at the end).<br />
<br />
> testK = eval (bot :: K P Q) :: P<br />
> testS = eval (bot :: S P Q R) :: App (App P R) (App Q R)<br />
<br />
Now I demonstrate several different ways of writing the identity combinator.<br />
<br />
> test1 = eval (bot :: I P) :: P<br />
> test2 = eval (bot :: C K0 I0 P) :: P<br />
> test3 = eval (bot :: App (Y KI0) P) :: P<br />
<br />
Axiomatic demonstrations of several other important combinators.<br />
<br />
> test4 = eval (bot :: M P) :: App P P<br />
> test5 = eval (bot :: W P Q) :: App (App P Q) Q<br />
> test6 = eval (bot :: C P Q R) :: App (App P R) Q<br />
> test7 = eval (bot :: B P Q R) :: App P (App Q R)<br />
<br />
Uncomment the following line to cause GHC to diverge.<br />
<br />
> -- testOmega = eval (bot :: OMEGA)<br />
<br />
Finally, a presentation of the church numerals in combinatory form.<br />
<br />
> type FoldN n = App (App n P) Q<br />
<br />
> type Z = SK0<br />
> type Succ0 = App S0 (App (App S0 KS0) K0)<br />
<br />
> type Plus0 = App (App S0 KS0) (App (App S0 (App K0 (App S0 (App K0 S0))))<br />
> (App S0 KK0))<br />
> type Mult0 = App (App S0 KS0) K0<br />
<br />
> type Succ a = App Succ0 a<br />
> type Mult n m = App (App Mult0 n) m<br />
> type Plus n m = App (App Plus0 n) m<br />
<br />
> type One = Succ Z<br />
> type Two = Succ One<br />
> type Three = Succ Two<br />
> type Four = Succ Three<br />
> type Five = Succ Four<br />
<br />
> test_n1 = eval (bot :: FoldN Z) :: Q<br />
> test_n2 = eval (bot :: FoldN One) :: App P Q<br />
<br />
> test_n3 = eval (bot :: FoldN (Plus Two Three))<br />
> test_n3 :: App P (App P (App P (App P (App P Q))))<br />
<br />
> test_n4 = eval (bot :: FoldN (Mult Two Four))<br />
> test_n4 :: App P (App P (App P (App P (App P (App P (App P (App P Q)))))))<br />
<br />
<br />
=================================================<br />
Appendix: definitions of additional combinators<br />
<br />
<br />
> type K x y = App (App K0 x) y<br />
> type S f g x = App (App (App S0 f) g) x<br />
> type I x = App SKK0 x<br />
> type B x y z = App (App (App B0 x) y) z<br />
> type C x y z = App (App (App C0 x) y) z<br />
> type M x = App M0 x<br />
> type W f x = App (App W0 f) x<br />
> type Y f = App Y0 f<br />
<br />
> type I0 = SKK0<br />
> type B0 = App (App S0 KS0) K0<br />
> type C0 = App (App S0 (App (App B0 B0) S0)) KK0<br />
> type W0 = App C0 (App (App B0 M0) (App (App B0 B0) (App C0 I0)))<br />
> type L0 = App (App C0 B0) M0<br />
> type Y0 = App (App S0 L0) L0<br />
> type KI0 = App K0 I0<br />
<br />
> type M0 = App (App S0 I0) I0<br />
> type OMEGA = App M0 M0<br />
<br />
> type KK0 = App K0 K0<br />
> type KS0 = App K0 S0<br />
> type KK x = App KK0 x<br />
> type KS x = App KS0 x<br />
<br />
> type SK0 = App S0 K0<br />
> type SS0 = App S0 S0<br />
> type SKK0 = App (App S0 K0) K0<br />
> type SKS0 = App (App S0 K0) S0<br />
> type SSK0 = App (App S0 S0) K0<br />
> type SSS0 = App (App S0 S0) S0<br />
> type SK f x = App (App SK0 f) x<br />
> type SS f x = App (App SS0 f) x<br />
> type SKK x = App SKK0 x<br />
> type SKS x = App SKS0 x<br />
> type SSK x = App SSK0 x<br />
> type SSS x = App SSS0 x</div>Robdockinshttps://wiki.haskell.org/index.php?title=Type_arithmetic&diff=5330Type arithmetic2006-08-11T12:43:43Z<p>Robdockins: </p>
<hr />
<div>'''Type arithmetic''' (or type-level computation) are calculations on<br />
the type-level, often implemented in Haskell using functional<br />
dependencies to represent functions.<br />
<br />
A simple example of type-level computation are operations on [[Peano numbers]]:<br />
<br />
data Zero<br />
<br />
data Succ a<br />
<br />
class Add a b ab | a b -> ab, a ab -> b<br />
instance Add Zero b b<br />
instance (Add a b ab) => Add (Succ a) b (Succ ab)<br />
<br />
Many other representations of numbers are possible, including binary and<br />
balanced base three. Type-level computation may also include type<br />
representations of boolean values, lists, trees and so on. It is closely<br />
connected to theorem proving, via<br />
[http://en.wikipedia.org/wiki/Curry-Howard the Curry-Howard isomorphism].<br />
<br />
A [http://okmij.org/ftp/Haskell/number-parameterized-types.html decimal representation] was put forward by [http://okmij.org/ftp/ Oleg Kiselyov] in [http://www.haskell.org/tmrwiki/NumberParamTypes "Number-Paramterized Types"] in the [http://www.haskell.org/tmrwiki/IssueFive fifth issue] of [http://www.haskell.org/tmrwiki/FrontPage The Monad Reader].<br />
<br />
== Library support ==<br />
<br />
Robert Dockins has gone as far as to write<br />
a [http://article.gmane.org/gmane.comp.lang.haskell.general/13206 library]<br />
for type level arithmetic, supporting the following operations on type<br />
level naturals: addition, subtraction, multiplication, division,<br />
remainder, GCD, and also contains the following predicates: test for<br />
zero, test for equality and < > <= >=<br />
<br />
This library uses a binary representation and can handle numbers at<br />
the order of 10^15 (at least). It also contains a test suite to help<br />
validate the somewhat unintuitive algorithms.<br />
<br />
== More type hackery ==<br />
<br />
Not to be outdone, Oleg Kiselyov has <br />
[http://article.gmane.org/gmane.comp.lang.haskell.general/13223 written]<br />
on invertible, terminating, 3-place addition, multiplication,<br />
exponentiation relations on type-level Peano numerals, where any two<br />
operands determine the third. He also shows the invertible factorial<br />
relation. Thus providing all common arithmetic operations on Peano<br />
numerals, including n-base discrete logarithm, n-th root, and the<br />
inverse of factorial. The inverting method can work with any<br />
representation of (type-level) numerals, binary or decimal.<br />
<br />
Oleg says, "The implementation of RSA on the type level is left for future work".<br />
<br />
== Djinn ==<br />
<br />
Somewhat related is Lennart Augustsson's tool <br />
[http://article.gmane.org/gmane.comp.lang.haskell.general/12747 Djinn], a theorem<br />
prover/coding wizard, that generates Haskell code from a given Haskell<br />
type declaration.<br />
<br />
Djinn interprets a Haskell type as a logic formula using<br />
[http://en.wikipedia.org/wiki/Curry-Howard the Curry-Howard isomorphism]<br />
and then a decision procedure for Intuitionistic Propositional Calculus.<br />
<br />
== An Advanced Example : Type-Level Quicksort ==<br />
<br />
An advanced example: quicksort on the type level.<br />
<br />
Here is a complete example of advanced type level computation, kindly<br />
provided by Roman Leshchinskiy. For further information consult Thomas<br />
Hallgren's 2001 paper <br />
[http://www.cs.chalmers.se/~hallgren/Papers/wm01.html Fun with Functional Dependencies]. <br />
<br />
module Sort where<br />
<br />
-- natural numbers<br />
data Zero<br />
data Succ a<br />
<br />
-- booleans<br />
data True<br />
data False<br />
<br />
-- lists<br />
data Nil<br />
data Cons a b<br />
<br />
-- shortcuts<br />
type One = Succ Zero<br />
type Two = Succ One<br />
type Three = Succ Two<br />
type Four = Succ Three<br />
<br />
-- example list<br />
list1 :: Cons Three (Cons Two (Cons Four (Cons One Nil)))<br />
list1 = undefined<br />
<br />
-- utilities<br />
numPred :: Succ a -> a<br />
numPred = const undefined<br />
<br />
class Number a where<br />
numValue :: a -> Int<br />
<br />
instance Number Zero where<br />
numValue = const 0<br />
instance Number x => Number (Succ x) where<br />
numValue x = numValue (numPred x) + 1<br />
<br />
numlHead :: Cons a b -> a<br />
numlHead = const undefined<br />
<br />
numlTail :: Cons a b -> b<br />
numlTail = const undefined<br />
<br />
class NumList l where<br />
listValue :: l -> [Int]<br />
<br />
instance NumList Nil where<br />
listValue = const []<br />
instance (Number x, NumList xs) => NumList (Cons x xs) where<br />
listValue l = numValue (numlHead l) : listValue (numlTail l)<br />
<br />
-- comparisons<br />
data Less<br />
data Equal<br />
data Greater<br />
<br />
class Cmp x y c | x y -> c<br />
<br />
instance Cmp Zero Zero Equal<br />
instance Cmp Zero (Succ x) Less<br />
instance Cmp (Succ x) Zero Greater<br />
instance Cmp x y c => Cmp (Succ x) (Succ y) c<br />
<br />
-- put a value into one of three lists according to a pivot element<br />
class Pick c x ls eqs gs ls' eqs' gs' | c x ls eqs gs -> ls' eqs' gs'<br />
instance Pick Less x ls eqs gs (Cons x ls) eqs gs<br />
instance Pick Equal x ls eqs gs ls (Cons x eqs) gs<br />
instance Pick Greater x ls eqs gs ls eqs (Cons x gs)<br />
<br />
-- split a list into three parts according to a pivot element<br />
class Split n xs ls eqs gs | n xs -> ls eqs gs<br />
instance Split n Nil Nil Nil Nil<br />
instance (Split n xs ls' eqs' gs',<br />
Cmp x n c,<br />
Pick c x ls' eqs' gs' ls eqs gs) =><br />
Split n (Cons x xs) ls eqs gs<br />
<br />
listSplit :: Split n xs ls eqs gs => (n, xs) -> (ls, eqs, gs)<br />
listSplit = const (undefined, undefined, undefined)<br />
<br />
-- zs = xs ++ ys<br />
class App xs ys zs | xs ys -> zs<br />
instance App Nil ys ys<br />
instance App xs ys zs => App (Cons x xs) ys (Cons x zs)<br />
<br />
-- zs = xs ++ [n] ++ ys<br />
-- this is needed because<br />
--<br />
-- class CCons x xs xss | x xs -> xss<br />
-- instance CCons x xs (Cons x xs)<br />
--<br />
-- doesn't work<br />
<br />
class App' xs n ys zs | xs n ys -> zs<br />
instance App' Nil n ys (Cons n ys)<br />
instance (App' xs n ys zs) => App' (Cons x xs) n ys (Cons x zs)<br />
<br />
-- quicksort<br />
class QSort xs ys | xs -> ys<br />
instance QSort Nil Nil<br />
instance (Split x xs ls eqs gs,<br />
QSort ls ls',<br />
QSort gs gs',<br />
App eqs gs' geqs,<br />
App' ls' x geqs ys) =><br />
QSort (Cons x xs) ys<br />
<br />
listQSort :: QSort xs ys => xs -> ys<br />
listQSort = const undefined<br />
<br />
And we need to be able to run this somehow, in the typechecker. So fire up ghci:<br />
<br />
> :t listQSort list1<br />
Cons<br />
(Succ Zero)<br />
(Cons (Succ One) (Cons (Succ Two) (Cons (Succ Three) Nil)))<br />
<br />
== A Really Advanced Example : Type-Level Lambda Calculus ==<br />
<br />
Again, thanks to Roman Leshchinskiy, we present a simple lambda calculus<br />
encoded in the type system (and with non-terminating typechecking fun!)<br />
<br />
Below is an example which encodes a stripped-down version of the lambda<br />
calculus (with only one variable):<br />
<br />
{-# OPTIONS -fglasgow-exts #-}<br />
data X<br />
data App t u<br />
data Lam t<br />
<br />
class Subst s t u | s t -> u<br />
instance Subst X u u<br />
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')<br />
instance Subst (Lam t) u (Lam t)<br />
<br />
class Apply s t u | s t -> u<br />
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'<br />
<br />
class Eval t u | t -> u<br />
instance Eval X X<br />
instance Eval (Lam t) (Lam t)<br />
instance (Eval s s', Apply s' t u) => Eval (App s t) u<br />
<br />
Now, lets evaluate some lambda expressions:<br />
<br />
> :t undefined :: Eval (App (Lam X) X) u => u<br />
undefined :: Eval (App (Lam X) X) u => u :: X<br />
<br />
Ok good, and:<br />
<br />
> :t undefined :: Eval (App (Lam (App X X)) (Lam (App X X)) ) u => u<br />
^CInterrupted.<br />
<br />
diverges ;)<br />
<br />
<br />
== Turing-complete example ==<br />
<br />
It's possible to embed the Turing-complete [[Type_SK|SK combinator calculus]] at the type level.<br />
<br />
== Theory ==<br />
<br />
See also [[dependent type]] theory.<br />
<br />
== Practice ==<br />
<br />
[[Extensible record]]s (which are used e.g. in type safe, declarative [[relational algebra]] approaches to [[Libraries and tools/Database interfaces|database management]])<br />
<br />
[[Category:Idioms]]</div>Robdockinshttps://wiki.haskell.org/index.php?title=Type_SK&diff=5329Type SK2006-08-11T12:38:51Z<p>Robdockins: A presentation of the SK combinator calculus at the type level</p>
<hr />
<div>Subject: [Haskell] The GHC typechecker is Turing-complete<br/><br />
Date: August 10, 2006 10:04:23 PM EDT<br />
<br />
This message is literate Haskell so you can all follow along at home.<br />
The program developed in this message was tested on GHC 6.4.2.<br />
<br />
My purpose today is to show that the GHC typechecker with multi-parameter<br />
typeclasses, functional dependencies, and undecidable instances is Turing-<br />
complete. Some time ago on this mailing list, there was a brief discussion<br />
about a lambda calculus and a direct Turing-machine implementation; either <br />
would be sufficient to demonstrate the Turing-completeness of the typechecker.<br />
However, neither implementation was preserved on-list, and the links are<br />
now dead.<br />
<br />
My strategy will be to embed the SK combinator calculus. The SK combinator<br />
calculus is capable of embedding the lambda calculus, which is well-known<br />
to be Turing-complete. Furthermore, the SK calculus is simpler to implement<br />
than the lambda calculus.<br />
<br />
For a complete proof of Turing-completeness, one should have a correctness<br />
proof for the embedding. I do not undertake such a proof here, but I will<br />
demonstrate what I hope to be convincing evidence for the correctness of<br />
this embedding.<br />
<br />
<br />
I begin by throwing the switches that give me the needed extensions.<br />
<br />
> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}<br />
> module SK where<br />
<br />
Next I define the terms of the SK combinator basis. This includes symbols for<br />
the combinators themselves, a symbol for application, and a way to introduce<br />
arbitrary uninterpreted types into computations.<br />
<br />
> data K0 <br />
> data S0<br />
> data App x y<br />
> data Other a<br />
<br />
Now I proceed to create the evaluator by first defining a single-step reduction<br />
relation. This relation is carefully designed to be reflexive on normal forms,<br />
and always reduces the leftmost-outermost redex. I then form the final<br />
evaluation relation by taking the transitive closure of single-step reduction.<br />
<br />
The semantics of typeclass constraint satisfaction are basicly strict. That<br />
is, the typechecker will make sure to fully evaluate all class constraints<br />
and fully instantiate all types whether or not those types turn out to be<br />
needed. Because of this, I need to be careful to form the transitive closure<br />
in a way that doesn't cause the typechecker to diverge on evaluation when it<br />
should not (of course, the typecheker will diverge on divergent terms).<br />
<br />
In order to do this, I define the single-step reduction relation so that it<br />
returns an additional result in addition to the reduced term. This result<br />
indicates 'More' whenever a redex was found and reduced and 'Done' otherwise.<br />
<br />
A few reduction rules perform reduction in parallel. These rules will return<br />
'More' if reduction was performed on any subterm.<br />
<br />
> data Done<br />
> data More<br />
<br />
> class CombineDone d1 d2 d | d1 d2 -> d<br />
> instance CombineDone Done Done Done<br />
> instance CombineDone Done More More<br />
> instance CombineDone More Done More<br />
> instance CombineDone More More More<br />
<br />
<br />
The 'Eval1' relation performs a single step of reduction. The presentation<br />
of this relation is somewhat tedious because we are forced to enumerate each<br />
possible spine shape up to 4 'App's deep. I could possibly do this more<br />
concisely if I enabled overlapping instances.<br />
<br />
> class Eval1 x y d | x -> y d<br />
<br />
I start by providing axioms stating that atomic terms evaluate to themselves<br />
with no reduction.<br />
<br />
> instance Eval1 S0 S0 Done<br />
> instance Eval1 K0 K0 Done<br />
> instance Eval1 (Other a) (Other a) Done<br />
<br />
There are a number of cases which just propagate evaluation contexts underneath<br />
the right-hand side of of 'App' when the spine shape cannot be reduced any<br />
further. These fairly uninteresting cases are collected together here.<br />
<br />
> instance Eval1 x x' d => Eval1 (App K0 x) (App K0 x') d<br />
> instance Eval1 x x' d => Eval1 (App S0 x) (App S0 x') d<br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , CombineDone d1 d2 d<br />
> ) => Eval1 (App (App S0 x) y) (App (App S0 x') y') d<br />
><br />
> instance Eval1 x x' d => Eval1 (App (Other a) x) (App (Other a) x') d<br />
> <br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , CombineDone d1 d2 d<br />
> ) => Eval1 (App (App (Other a) x ) y )<br />
> (App (App (Other a) x') y') d<br />
><br />
> instance ( Eval1 x x' d1<br />
> , Eval1 y y' d2<br />
> , Eval1 z z' d3<br />
> , CombineDone d1 d2 d4<br />
> , CombineDone d3 d4 d<br />
> ) => Eval1 (App (App (App (Other a) x ) y ) z )<br />
> (App (App (App (Other a) x') y') z') d<br />
<br />
Now we get to the real meat. Here are the rules for reducing the 'K'<br />
combinator. There are rules for reducing under both 2 and 3 'App's.<br />
<br />
> instance Eval1 (App (App K0 x) y) x More<br />
> instance Eval1 (App (App (App K0 x) y) z) (App x z) More<br />
<br />
And here, the rule for reducing the 'S' combinator.<br />
<br />
> instance Eval1 <br />
> (App (App (App S0 f) g) x)<br />
> (App (App f x) (App g x))<br />
> More<br />
<br />
Finally, a rule to decompose an arbitrary 'App' context. I propagate<br />
the evaluation context down the left side of an 'App' only when that<br />
'App' is not involved in any redexes. This implements the leftmost-<br />
outermost strategy. In any leftmost spine consisting of 4 'App's,<br />
the leftmost 'App' can never be involved in any redex. The cases for<br />
other levels of 'App's are folded into the above rules.<br />
<br />
> instance ( Eval1 (App (App (App p q) x) y) a d<br />
> ) => Eval1 (App (App (App (App p q) x) y) z) (App a z) d<br />
<br />
<br />
Now I need to take the transitive closure of the 'Eval1' relation. I do<br />
this with the auxiliary 'EvalAux' class. The first instance represents<br />
the base case, where 'Eval1' performed no reductions. The second instance<br />
implements the transitivity and does bookkeeping with the termination markers.<br />
<br />
> class EvalAux x y q1 | x q1 -> y<br />
><br />
> instance EvalAux x x Done<br />
><br />
> instance ( Eval1 x y q<br />
> , EvalAux y z q<br />
> ) => EvalAux x z More<br />
<br />
<br />
Now at last I can define the evaluation relation. It is defined in terms of<br />
'EvalAux' and hides the termination bookkeeping.<br />
<br />
> class Eval x y | x -> y<br />
> instance EvalAux x y More => Eval x y<br />
<br />
<br />
I define convenient functions to allow me to invoke the type evaluators<br />
and a synonym for 'undefined' to cut down on typing.<br />
<br />
> eval1 :: Eval1 x y q => x -> y<br />
> eval1 = undefined<br />
<br />
> eval :: Eval x y => x -> y<br />
> eval = undefined<br />
<br />
> bot :: a<br />
> bot = undefined<br />
<br />
Before showing off the evaluator, I'm going to need several dummy types<br />
to work with.<br />
<br />
> data P0<br />
> data Q0<br />
> data R0<br />
<br />
> type P = Other P0<br />
> type Q = Other Q0<br />
> type R = Other R0<br />
<br />
Now, some examples of the SK evaluator in action. First I show<br />
that the S and K combinators have their expected axiomatic behavior.<br />
(Note, the following demonstrations rely on definitions found in the<br />
appendix at the end).<br />
<br />
> testK = eval (bot :: K P Q) :: P<br />
> testS = eval (bot :: S P Q R) :: App (App P R) (App Q R)<br />
<br />
Now I demonstrate several different ways of writing the identity combinator.<br />
<br />
> test1 = eval (bot :: I P) :: P<br />
> test2 = eval (bot :: C K0 I0 P) :: P<br />
> test3 = eval (bot :: App (Y KI0) P) :: P<br />
<br />
Axiomatic demonstrations of several other important combinators.<br />
<br />
> test4 = eval (bot :: M P) :: App P P<br />
> test5 = eval (bot :: W P Q) :: App (App P Q) Q<br />
> test6 = eval (bot :: C P Q R) :: App (App P R) Q<br />
> test7 = eval (bot :: B P Q R) :: App P (App Q R)<br />
<br />
Uncomment the following line to cause GHC to diverge.<br />
<br />
> -- testOmega = eval (bot :: OMEGA)<br />
<br />
Finally, a presentation of the church numerals in combinatory form.<br />
<br />
> type FoldN n = App (App n P) Q<br />
<br />
> type Z = SK0<br />
> type Succ0 = App S0 (App (App S0 KS0) K0)<br />
<br />
> type Plus0 = App (App S0 KS0) (App (App S0 (App K0 (App S0 (App K0 S0))))<br />
> (App S0 KK0))<br />
> type Mult0 = App (App S0 KS0) K0<br />
<br />
> type Succ a = App Succ0 a<br />
> type Mult n m = App (App Mult0 n) m<br />
> type Plus n m = App (App Plus0 n) m<br />
<br />
> type One = Succ Z<br />
> type Two = Succ One<br />
> type Three = Succ Two<br />
> type Four = Succ Three<br />
> type Five = Succ Four<br />
<br />
> test_n1 = eval (bot :: FoldN Z) :: Q<br />
> test_n2 = eval (bot :: FoldN One) :: App P Q<br />
<br />
> test_n3 = eval (bot :: FoldN (Plus Two Three))<br />
> test_n3 :: App P (App P (App P (App P (App P Q))))<br />
<br />
> test_n4 = eval (bot :: FoldN (Mult Two Four))<br />
> test_n4 :: App P (App P (App P (App P (App P (App P (App P (App P Q)))))))<br />
<br />
<br />
=================================================<br />
Appendix: definitions of additional combinators<br />
<br />
<br />
> type K x y = App (App K0 x) y<br />
> type S f g x = App (App (App S0 f) g) x<br />
> type I x = App SKK0 x<br />
> type B x y z = App (App (App B0 x) y) z<br />
> type C x y z = App (App (App C0 x) y) z<br />
> type M x = App M0 x<br />
> type W f x = App (App W0 f) x<br />
> type Y f = App Y0 f<br />
<br />
> type I0 = SKK0<br />
> type B0 = App (App S0 KS0) K0<br />
> type C0 = App (App S0 (App (App B0 B0) S0)) KK0<br />
> type W0 = App C0 (App (App B0 M0) (App (App B0 B0) (App C0 I0)))<br />
> type L0 = App (App C0 B0) M0<br />
> type Y0 = App (App S0 L0) L0<br />
> type KI0 = App K0 I0<br />
<br />
> type M0 = App (App S0 I0) I0<br />
> type OMEGA = App M0 M0<br />
<br />
> type KK0 = App K0 K0<br />
> type KS0 = App K0 S0<br />
> type KK x = App KK0 x<br />
> type KS x = App KS0 x<br />
<br />
> type SK0 = App S0 K0<br />
> type SS0 = App S0 S0<br />
> type SKK0 = App (App S0 K0) K0<br />
> type SKS0 = App (App S0 K0) S0<br />
> type SSK0 = App (App S0 S0) K0<br />
> type SSS0 = App (App S0 S0) S0<br />
> type SK f x = App (App SK0 f) x<br />
> type SS f x = App (App SS0 f) x<br />
> type SKK x = App SKK0 x<br />
> type SKS x = App SKS0 x<br />
> type SSK x = App SSK0 x<br />
> type SSS x = App SSS0 x</div>Robdockinshttps://wiki.haskell.org/index.php?title=File:Num-bytecodes.txt&diff=5187File:Num-bytecodes.txt2006-08-04T16:00:35Z<p>Robdockins: A proposal for revamping the numeric bytecodes in Yhc.</p>
<hr />
<div>A proposal for revamping the numeric bytecodes in Yhc.</div>Robdockinshttps://wiki.haskell.org/index.php?title=Talk:History_of_Haskell/Version_1&diff=4935Talk:History of Haskell/Version 12006-07-19T18:50:23Z<p>Robdockins: </p>
<hr />
<div>== Comments on "The History of Haskell" (draft) ==<br />
<br />
Please use the Wiki to add your comments here. Include your name and the date. You can do this with four tildes, like this: <nowiki>~~~~</nowiki>.<br />
<br />
To edit the page, you need to log in: click the login link at the bottom of the window. If you don't already have an account, the login page lets you create one in 30 seconds. See [[HaskellWiki:Contributing]].<br />
<br />
-----------------<br />
<br />
== Administration ==<br />
<br />
[[User:Simonpj|Simonpj]] 18:51, 14 July 2006 (UTC) Simon PJ. Here is an example comment<br />
<br />
[[User:BerniePope|BerniePope]] I hope you don't mind, but I've taken the liberty of breaking this up into sections, so that it is easier to find out what has been said already. This seems to be especially useful for typos etc. Please feel free to add other sections if you think they are necessary. I've also made the page numbers bold, and put them into page order (where possible).<br />
<br />
== Title suggestions ==<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 20:38, 14 July 2006 (UTC) Other ideas for a title: ''The History of Haskell: Unsuccessfully Avoiding Success'' or something using the motto "Avoid success at all costs." Or perhaps ''Success Considered Harmful, or, A History of Haskell'' or ''Doomed to Succeed'' quoting Hoare (although this sounds somewhat self-congratulatory).<br />
<br />
[[User:GaneshSittampalam|GaneshSittampalam]] 09:19, 15 July 2006 (UTC) I really like the "eager to be lazy" title.<br />
<br />
[[User:BerniePope|BerniePope]] 13:59, 17 July 2006 (UTC) Subtitles: (not serious) "A pure type of fun, with no side-effects (except when bottoms are uncovered)". "From theorems to tools". "Doing lots of typing to avoid doing lots of work". "Beta reduction than destructive update". <br />
<br />
== Typos, spelling, grammar, formatting and expression ==<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Typo: '''page 2''', column 2, "Rod Bustall" should be "Rod Burstall".<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Spelling: '''page 3''', column 1, "confernce".<br />
<br />
On '''page 4''' after the list of goals, it seems that the following sentence ("We agreed to base it on an existing language,<br />
namely OL.") should be preceeded by a line break (it now starts on the same line as the sixth goal).<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 22:00, 14 July 2006 (UTC) '''page 9''' Section 3.8, last paragraph, syntax error: should be "Miranda is still in use today: it '''is''' still taught in some institutions", missing word. (Sec 4.2 ''This tradition was honed by Moses Schonfinkel and Haskell Curry, and came to be called currying.'' I half expected a joke following this, saying ''[it was] called currying, luckily, and not '''schonfinkeling'''.'') Same section, typo: ''is a list of lists'' should be ''in a list of lists.''<br />
:That joke would have been surpassed by reality, because the german word for ''currying'' '''is''' ''schÃ¶nfinkeln''. See [http://de.wikipedia.org/wiki/Sch%C3%B6nfinkeln SchÃ¶nfinkeln]. --[[User:MarcVanWoerkom|MarcVanWoerkom]] 18:49, 16 July 2006 (UTC)<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Expression. '''page 9'''. It says "Haskell did not adopt Miranda's abstract data types, using '''its''' module system instead." It is not clear whose module system it is using. Perhaps it should read "using '''a''' module system instead." ?<br />
<br />
[[User:BerniePope|BerniePope]] 15:56, 15 July 2006 (UTC) Tense. '''page 12'''. Section 5.1, algebraic data types. It says "In general, every algebraic data type specified...", should that be "specifies" ? or perhaps even better "In general, algebraic data types specify" ?<br />
<br />
[[User:Ruiz|Ruiz]] 12:04, 16 July 2006 (UTC) Comment. '''page 12'''. If I am not mistaken, the Fermat's Last Theorem example only generates (1,1,z) triplets.<br />
<br />
[[User:BerniePope|BerniePope]] 16:15, 15 July 2006 (UTC) Tense. '''page 13'''. Section 5.3 Abstract types. It says "This had the advantage ...". Perhaps it should be: "This has the advantage", since Miranda still exists, and the advantage still holds. Later in the same paragraph the expression about adopting the feature in Haskell is a bit awkward. Perhaps it could read: "It is not clear how to adapt Miranda's method of defining abstract data types to type classes, and that is one reason we chose a different solution." ?<br />
<br />
[[User:BerniePope|BerniePope]] 16:27, 15 July 2006 (UTC) Typo. Section 5.6, '''page 14''' and in Bibliography. Godel's name in citation missing the 'o'.<br />
<br />
[[User:BerniePope|BerniePope]] 05:41, 16 July 2006 (UTC) Comment. '''page 15''', column 1. "practical comprehensibility" is a bit of a mouthful. Perhaps "pragmatism" would suffice?<br />
<br />
[[User:BerniePope|BerniePope]] 06:11, 16 July 2006 (UTC) Typo (possibly). '''page 16'''. Section 6.4, multi-parameter type classes. "They gave the following example: second.". Should the "second" be there?<br />
<br />
[[User:BerniePope|BerniePope]] 06:56, 16 July 2006 (UTC) Typo, '''page 16'''. The code "n = (x + y)", perhaps drop the redundant parens?<br />
<br />
[[User:BerniePope|BerniePope]] 07:19, 16 July 2006 (UTC) '''page 17'''. Choice of identifier. In the code "f (MkT x f) = f x". Perhaps the inner or outer "f" should be renamed? Also, is there a more compelling example than this one?<br />
<br />
[[User:Weihu|Weihu]] 17:33, 16 July 2006 (UTC) '''page 17'''. Duplication of words. "The the type qualification in this case" => "The type qualification in this case".<br />
<br />
[[User:BerniePope|BerniePope]] 07:16, 16 July 2006 (UTC) Typo. '''page 17'''. "patter-matching" -> "pattern-matching".<br />
<br />
[[User:BerniePope|BerniePope]] 07:26, 16 July 2006 (UTC) Expression. '''page 17'''. Perhaps drop "rather than explicitly". This is implied by the previous "happens implicitly".<br />
<br />
[[User:BerniePope|BerniePope]] 07:38, 16 July 2006 (UTC) Typo. '''page 18'''. In lexically scoped type variables, it says the type of xcons is "forall a. a -> a". Do you mean: "forall a . [a] -> [a]"?<br />
<br />
[[User:Plareplane|Plareplane]] 01:13, 18 July 2006 (UTC) Typo. '''page 20'''. "The input in the string to be parsed, and returns a list of parse results, consisting of the value parsed and the remaining unparsed string."<br />
<br />
[[User:BerniePope|BerniePope]] 08:39, 16 July 2006 (UTC) Typesetting. '''page 22'''. Sometimes the "IO monad" is written where "IO" is in typewriter font, and other times it is in times roman, and other times it is written "I/O". This may be an intentional distinction, but maybe the notation can be unified?<br />
<br />
[[User:Weihu|Weihu]] 20:36, 16 July 2006 (UTC) Word missing. '''page 22'''. "So readFile a function that" => "So readFile is a function that".<br />
<br />
[[User:ChristianSievers|ChristianSievers]] 18:20, 18 July 2006 (UTC) Word too much. '''page 22'''. "An IO computation is a function that (logically) takes a the state..." Drop "a" or "the".<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 04:27, 15 July 2006 (UTC) '''page 25'''. Section 9.2 misspelling "existance" should be "existence" third to last paragraph. Sec. 9.5 , '''page 27''', second to last paragraph. ''test bad'' should be ''test bed''.<br />
<br />
[[User:BerniePope|BerniePope]] 12:33, 16 July 2006 (UTC) Typo. '''page 28'''. Section 10.2, paragraph 2. "who had by thus time" -> "who had by this time".<br />
<br />
[[User:BerniePope|BerniePope]] 13:22, 16 July 2006 (UTC) Missing word. '''page 30'''. Section 10.4.2 Observational debugging. It says "to track down bug location" -> "to track down '''the''' bug location".<br />
<br />
[[User:BerniePope|BerniePope]] 05:07, 17 July 2006 (UTC) Expression. '''page 30'''. Section 10.5 Testing tools. "If debugging tools ... -> "Whilst debugging tools ...". The "if" seems to be left hanging in the sentence.<br />
<br />
[[User:BerniePope|BerniePope]] 05:30, 17 July 2006 (UTC) Syntax. '''page 30'''. Section 10.5 Testing tools. In the definition of "prop_insert" you use "$" for infix application, and thus avoid some parens. I wonder whether it would be better to have the explicit parens instead? Non Haskellers may find the "$" style difficult to parse. Also, it would be more consistent with other example pieces of code in the paper.<br />
<br />
[[User:Weihu|Weihu]] 21:35, 15 July 2006 (UTC) Typo: '''page 31''', column 2, "a central them" should be "a central theme".<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:14, 18 July 2006 (UTC) Typo: '''page 32''' end of page. Unless my PDF reader is missed up (likely) "time = Beh (\t - t)" should be "time = Beh (\t -> t)".<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:18, 18 July 2006 (UTC) Typo. '''page 33''' Second paragraph, 11.2.2 "Arguably, in is better" should be "Arguably, it is better".<br />
<br />
[[User:BerniePope|BerniePope]] 05:47, 17 July 2006 (UTC) Typo. '''page 33'''. Section 11.2.1 Functional reactive programming. The instance declaration for Floating is missing "Behaviour a) where".<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:24, 18 July 2006 (UTC) Typo. '''page 33'''. sec 11.2.3: First three sentences could perhaps be combined with colons and semicolons, i.e. "Lazy functional [snip]: firstly [snip]; secondly [snip]." or the the second and third sentence fragments might be provided with predicates.<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:31, 18 July 2006 (UTC) Typo. '''page 34'''. sec. 11.2.3 end of first paragraph <pre>Microsoft?".</pre> should be <pre>Microsoft?"</pre> (omit period after quote).<br />
<br />
[[User:GaneshSittampalam|GaneshSittampalam]] 09:18, 15 July 2006 (UTC) Section 11.2.3 '''page 34''' typo "unsagePerformIO".<br />
<br />
[[User:BerniePope|BerniePope]] 06:44, 17 July 2006 (UTC) Missing word (perhaps). '''page 34'''. Section 11.2.5 Summary. It says "... a DSEL is little than that." I have not heard that expression before, perhaps it was meant to be: "... a DSEL is little '''more''' than that."? <br />
<br />
[[User:BerniePope|BerniePope]] 06:51, 17 July 2006 (UTC) Typo. '''page 35'''. Section 11.3 Graphical user interfaces. "lacked the fully range of widgets" -> "lacked the '''full''' range of widgets".<br />
<br />
[[User:BerniePope|BerniePope]] 06:54, 17 July 2006 (UTC) Extra word. '''page 35'''. Section 11.3 Graphical user interfaces. "... and '''only''' implemented '''only''' part of the full interface."<br />
<br />
[[User:Weihu|Weihu]] 21:42, 16 July 2006 (UTC) '''page 35''': "invariably based on a imperative widget" => "invariably based on an imperative widget".<br />
<br />
[[User:BerniePope|BerniePope]] 06:54, 17 July 2006 (UTC) Typo. '''page 35'''. Section 11.4 Natural language processing. "Callaghan?s": there is a question mark where there ought to be an apostrophe.<br />
<br />
[[User:BerniePope|BerniePope]] 07:07, 17 July 2006 (UTC) Notation. '''page 36'''. Section 12.1 Education. You write "embedded DSLs", earlier in Section 11.2 you use the acronym "DSEL" perhaps for the same thing?<br />
<br />
[[User:BerniePope|BerniePope]] 07:14, 17 July 2006 (UTC) Typo (possibly). '''page 36'''. Section 12.1.1 A survey of Haskell in Higher Education. On my screen it looks like there is an extra space after the number 28, in the sentence "Surprisingly, only 28 ..." Perhaps there is supposed to be a percent sign in there? Could be an artefact of the PDF viewer i'm using, but seems unlikely.<br />
<br />
[[User:BerniePope|BerniePope]] 07:21, 17 July 2006 (UTC) Typo. '''page 36'''. Section 12.1.1 A survey of Haskell in Higher Education. Bottom of second column. Backwards quotation marks at start of "The students who take the Haskell track ..."<br />
<br />
[[User:BerniePope|BerniePope]] 07:56, 17 July 2006 (UTC) Missing word. '''page 37'''. Section 12.2 Haskell and software productivity. "These contests have open to anyone." -> "These contests have '''been''' open to anyone."<br />
<br />
[[User:BerniePope|BerniePope]] 08:03, 17 July 2006 (UTC) Typo, '''page 37'''. Section 12.3. Darcs and Pugs. Third paragraph. "source coded" -> "source code".<br />
<br />
[[User:BerniePope|BerniePope]] 08:25, 17 July 2006 (UTC) Expression (minor). '''page 38'''. Section 12.4.2 Bluespec. "The purpose of them" -> "Their purpose". Later in the same paragraph there is a typo: "Haskell language construct" -> "Haskell language constructs" (plural). <br />
<br />
Typo on '''page 39''': Another example is that Linspires ''toold'' must handle legacy data formats. --[[User:NeilMitchell|Neil Mitchell]] 15:23, 14 July 2006 (UTC)<br />
<br />
[[User:Plareplane|Plareplane]] 01:13, 18 July 2006 (UTC) Extra word. '''page 40'''. "given we the importance we usually attach"<br />
<br />
Typo on '''page 43''': Missing letter in "Gdel". [[User:Phlucas|Phlucas]] 09:54, 17 July 2006 (UTC)<br />
<br />
Two different papers are referenced as (Kiselyov et. al. 2004) in the text (bib entries on '''page 44'''). [[User:Phlucas|Phlucas]] 09:54, 17 July 2006 (UTC)<br />
<br />
Duplicate reference Wallace/Chitil/Brehm/Runciman on '''page 48'''. [[User:Phlucas|Phlucas]] 09:54, 17 July 2006 (UTC)<br />
<br />
[[User:BerniePope|BerniePope]] 13:06, 16 July 2006 (UTC) Overall. Capitalisation in headings seems to be inconsistent.<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:51, 18 July 2006 (UTC) Many places, esp. sec. 12. The word "textbook" appears as "text book" and "text-book" although I believe "textbook" is the textbook spelling.<br />
<br />
[[User:JevgeniKabanov|JevgeniKabanov]] 15:58, 18 July 2006 (UTC) Page 25 has transactional '''mememory'''.<br />
<br />
== General comments ==<br />
<br />
[[User:Padator|Padator]] 08:56, 17 July 2006 (UTC) '''Page 7'''. There is maybe too few discussions about the work of Stefan Kaes. I would like to know more about this topic.<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Comment. '''page 7'''. Section 3.3, third paragraph. Rather than talk about "div" (are the first quote marks backwards?), perhaps you could say - "for example, Miranda's type system allows floating point values to be given to functions which are only defined on the integer subset of num, thus turning a static error into a dynamic one."<br />
<br />
[[User:BerniePope|BerniePope]] 04:24, 18 July 2006 (UTC) Comment. '''page 9'''. Section 4 Syntax. I was a little surprised not to see a discussion of the literate style. Though it is not a Haskell invention, it still seems important.<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Comment. '''page 10'''. Section 4.1, layout. It says "The rules are simple ...". I think this is a contentious issue. Recent discussions on the Haskell Prime mailing list [http://www.haskell.org//pipermail/haskell-prime/2006-March/000898.html] suggested a contrary view. How many Haskellers actually know the rules? Perhaps it would be more accurate to say that experience shows it is not hard to adopt a style of programming which stays within the rules.<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Comment. Footnote 2 on '''page 10''' says the Scheme authors took a more Draconian approach with respect to operators, though it doesn't actually say what that means. On the off chance that someone reading the paper doesn't know Scheme, it might be worth elaborating on that point.<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Comment. '''page 12'''. Section 4.4. Near the end of the section you give an example of "where" being attached to a declaration. I think the example function "f" is rather obscure, perhaps there is a better example? Maybe one from the Prelude? Also, there seems to be another point you could make here. Due to laziness we get some more freedom in the way that we write where clauses. For instance, the thing being defined in the where clause may only be well defined in a subset of the alternatives. But that doesn't matter because we will only evaluate the thing if and when it is needed, not before.<br />
<br />
[[User:BerniePope|BerniePope]] 15:42, 15 July 2006 (UTC) Comment. '''page 12'''. Section 4.5, list comprehensions. Perhaps it is worth noting the Haskell does not have the diagonalisation operator like Miranda. It may also be worth remarking on why this is so. Surely it was considered.<br />
<br />
[[User:BerniePope|BerniePope]] 16:05, 15 July 2006 (UTC) Comment. '''page 13'''. Section 5.3 Abstract types. It says that the type has one constructor. Is it really necessary to limit the type to just one constructor? Surely it is enough that the constructors of the type are not exported, regardless of how many there are?<br />
<br />
[[User:BerniePope|BerniePope]] 13:24, 17 July 2006 (UTC) Comment. '''page 14'''. Section 6 Haskell as a type system laboratory. You don't seem to mention the defaulting rules of Haskell for unresolved numeric overloading. Whilst I think defaulting is somewhat of a wart, it is nonetheless of interest because it reveals some of the difficult design decisions that have to be made in the definition of a real programming language. Some of the most interesting parts of this paper are the sections which delve into the process of designing the features of Haskell, and maybe the defaulting story is worth telling too.<br />
<br />
[[User:BerniePope|BerniePope]] 05:28, 16 July 2006 (UTC) Comment. '''page 14'''. Section 6.1, Type classes. Perhaps it should mention that '''eqInt''' is primitive equality on integers, maybe as a comment in the code.<br />
<br />
[[User:BerniePope|BerniePope]] 05:54, 16 July 2006 (UTC) Comment. '''page 15'''. Section 6.2 Monomorphism restriction. This marks one of the most unusual aspects of the language, especially in the Language Report. In particular, it is motivated by operational semantics --- sharing --- but the rest of the Report is largely silent on the issue. I think the Report says something to the effect of "programmers expect sharing to be preserved", but there is not much else in the Report to back this statement up. Perhaps you could tie this back to the discussion in Section 3.4 (Haskell has no formal semantics). Also, I think it would be reasonable to say "GHC provides a flag to suppress the restriction", without actually naming the flag.<br />
<br />
[[User:BerniePope|BerniePope]] 06:02, 16 July 2006 (UTC) Comment. '''page 15'''. Section 6.2 Higher kinded polymorphism. It says "Here, the type variable m has kind *->*". It seems like the reader is already supposed to know what a kind is at this point. Perhaps the section could provide a little introduction to the concept of kinds first. Another thing about kinds is that they are sort of shadowy figures that seem to lurk in the background of Haskell. For instance they have no syntactic counterpart in Haskell 98. It can be quite daunting for beginners when they get a kind error.<br />
<br />
[[User:BerniePope|BerniePope]] 07:30, 16 July 2006 (UTC) Comment. '''page 17'''. Section 6.6 Implicit parameters. Perhaps contrast this approach to a Reader monad?<br />
<br />
[[User:BerniePope|BerniePope]] 07:44, 16 July 2006 (UTC) Comment. '''page 18'''. Arrows. It doesn't really say what arrows are, except that they are like monads, but more general. Perhaps this could be elaborated, maybe with some mention of the intuition that arrows generalise things which are somehow composable? Perhaps an example of an arrow which cannot be done with a monad?<br />
<br />
[[User:BerniePope|BerniePope]] 08:14, 16 July 2006 (UTC) Comment. '''page 20'''. Section 7.2 Monads. It says that "Checking that the laws hold provides a reassuring sanity check when defining a new monad." Perhaps you could elaborate on exactly what we are checking, and subsequently reassured about. It says earlier that the laws show associativity and identity, but is there a more "programmer oriented" view of what this means? <br />
<br />
[[User:BerniePope|BerniePope]] 08:22, 16 July 2006 (UTC) Comment. '''page 20'''. Section 7.2 Monads. It says monads were helpful in structuring programs, including "the Haskell compiler itself". This sounds like there was a single Haskell compiler. Perhaps it should be "exisiting Haskell compilers"?<br />
<br />
[[User:BerniePope|BerniePope]] 08:22, 16 July 2006 (UTC) Comment. '''page 20'''. Section 7.2 Monads. One of the ongoing issues with monads is combining them together. Perhaps you could mention some of the attempts at doing this, such as monad transformers.<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 23:16, 17 July 2006 (UTC) Comment. '''page 21'''. While reading and referring to the figures I keep getting confused by which Figure is Figure 2, Figure 3, etc. due to the heavy black lines which seem to act as separators, forcing my brain into believing that the heading applies to the code below the black line. Although I looked at the page as a whole to know which heading belongs to which figure, subconciously I am still confused by the dividing lines and automatically read the wrong heading for each section. Perhaps moving the lines, introducing a second set of lines above each section of code, or careful use of more whitespace (or complete boxes?) could alieviate or disambiguate these figures?<br />
<br />
[[User:BerniePope|BerniePope]] 08:30, 19 July 2006 (UTC) Comment. '''page 24'''. Section 8.2.3 Summary. It says "a glance at the literature on ML modules will confirm" (regarding making things easier). Perhaps you could back this up with a sample of some references?<br />
<br />
[[User:BerniePope|BerniePope]] 13:04, 16 July 2006 (UTC) Comment. '''page 29'''. Section 10.3 Controlling Evaluation Order. The last paragraph suggests that we can wait until the program is written, then profile, then add seqs as necessary. While this is true, many programs are never really finished. Adding seq to code is one thing, but maintaining code with seq in it is another, perhaps more difficult problem. Also, you might be able to make a link here to the material on speculative evaluation, since that also solves some space/strictness issues.<br />
<br />
[[User:BerniePope|BerniePope]] 13:14, 16 July 2006 (UTC) Comment. '''page 29'''. Section 10.4 Debugging and tracing. It says that hbc and GHC provide trace. Hugs also has trace (perhaps nhc98 does as well?).<br />
<br />
[[User:BerniePope|BerniePope]] 04:59, 17 July 2006 (UTC) Comment. '''page 30'''. Section 10.4.2 Observational debugging. In the Hood library the type of observe is overloaded, like "observe :: Observeable a => String -> a -> a", which is both an interesting and useful application of type classes, and in some ways a limitation of hood, since it isn't polymorphic. I think it is important to point out the use of overloading here. Also, I think Hugs comes with a built-in polymorphic version, which of course isn't portable.<br />
<br />
[[User:Hoan|Hoan]] 12:45, 15 July 2006 (UTC) On '''page 33''' it says that Ruby on Rails is a continuation based framework. I think thats wrong. PS. Its a riveting read.<br />
<br />
[[User:BerniePope|BerniePope]] 08:38, 17 July 2006 (UTC) Comment. '''page 37'''. Section 12.4 Companies using Haskell. Perhaps you could mention the Commerical users of FP workshop? Not limited to Haskell, but an important sign of a coming of age.<br />
<br />
[[User:BerniePope|BerniePope]] 08:22, 17 July 2006 (UTC) Comment. '''page 38'''. Section 12.4.2 Bluespec. It says "The type system has been extended with types of numeric kind." Perhaps this could be reworded to avoid the use of "kind", which has a specific meaning in types. Unless of course it does actually mean "kind" in the specific sense. Either way it could probably be clarified.<br />
<br />
[[User:BerniePope|BerniePope]] 13:29, 17 July 2006 (UTC) Comment '''page 39'''. Section 12.5 The Haskell community. Perhaps you could also mention the Haskell IRC channel [http://www.haskell.org/haskellwiki/IRC_channel], and some of its interesting software clients, especially lambdabot.<br />
<br />
[[User:BerniePope|BerniePope]] 08:46, 17 July 2006 (UTC) Comment (not serious). '''page 39'''. Section 12.5 The Haskell community. It says that the Haskell Cafe' is most active in winters, with an amusing footnote about Scandinavia. Don't forget that in the southern hemisphere we have winter at the opposite time of the year! There are lots of Haskellers down here too! Also, if the winter connection is true, then it doesn't bode well for the adoption of Haskell in countries like Singapore and Indonesia.<br />
<br />
[[User:Saccade|Saccade]] 20:57, 17 July 2006 (UTC) Comment '''page 39''' Section 12.5 The Haskell community. Footnote 14 is a lot more important than you seem to be giving it credit for. Polyglot programmers (like me) have a strong tendency to pick up new languages with great enthusiasm, and then ditch them a few years later with equally great enthusiasm. A reasonable null hypothesis model would be that about n_0 =~ 600 people get seriously into Haskell every year, and then have a roughly k =~ 4/5 chance of ditching the language for each year thereafter, giving n_t == n_0 * k^t serious users who have been using it for t years. This comes out looking a lot like your graph. (I'm not saying it's not possible that there's an explosion of interest, but this isn't very good evidence for it.)<br />
<br />
[[User:BerniePope|BerniePope]] 08:59, 17 July 2006 (UTC) Comment. '''page 40'''. Section 12.6. Influence on other languages. Maybe you can mention that Clean has a powerful system of dynamic types, and also generic functions which go beyond type classes. Also, since you mention that Clean has an I/O system based on linear types, you might also like to mention that Mercury also takes a similar approach, using unique modes.<br />
<br />
[[User:BerniePope|BerniePope]] 09:08, 17 July 2006 (UTC) Comment. '''page 41'''. Section 13. Acknowledgements. In the last paragraph you note all the people who have contributed material, but you do not mention Nikhil, who is cited on page 38 as contributing the section on BlueSpec.<br />
<br />
[[User:BerniePope|BerniePope]] 07:57, 16 July 2006 (UTC) Overall. Names of people. I've noticed that sometimes people are referred to by their whole name, whilst others are referred to by just their family name. Perhaps there is an underlying method here, but it wasn't clear to me. Perhaps it is that the first reference gets a full name, and subsequent ones are just the family name? Is that always the case?<br />
<br />
[[User:Abayley|Abayley]] 07:37, 17 July 2006 (UTC) JHC gets a one-line mention - perhaps it deserves a little more? AFAICT, it was written by one person, as a student, who decided that the best way to learn Haskell was by writing a Haskell compiler. A commendable effort I think, and also a testament to the power of the language.<br />
<br />
[[User:BerniePope|BerniePope]] 13:39, 17 July 2006 (UTC) Comment. Overall. The paper seems to be missing a conclusion at the end. Something to tie it all together. I was hoping to read a little bit about what the future of Haskell may bring - even though it would only be speculation, it would still be useful. What are the lessons learned? What would you do differently, now that you have the benefit of hindsight? Are we doomed to keep inventing programming languages? What does Haskell still need?<br />
<br />
[[User:AndrePang|AndrePang]] 00:45, 18 July 2006 (UTC) Comment. I'm not sure if this is appropriate for this paper, but perhaps a mention of significant papers to come out of GHC work would be good. The example I had in mind was pioneering garbage collection techniques, but there may also be other areas that are applicable. Even if it's a one or two paragraph blurb on it, it'd add to the impression that GHC is, in fact, a state-of-the-art compiler. For what it's worth, I also agree with Alistair Bayley about giving GHC more than a one-line blurb: it's an impressive piece of work with courageous goals.<br />
<br />
[[User:JaredUpdike|JaredUpdike]] 00:49, 18 July 2006 (UTC) Question. Where is the standard "Miranda is a trademark of Research Ltd." disclaimer? Is it unnecessary given the fact that the history of Miranda is recounted and Turner given due credit?<br />
<br />
[[User:BerniePope|BerniePope]] 04:14, 18 July 2006 (UTC) Comment. Diagrams! I think a really useful addition to this paper would be a couple of diagrams. First, a timeline of the developments of Haskell. To help us put the whole thing in perspective. You could annotate the timeline with version numbers, interesting developments (like monads etc), major compiler/tool releases, significant events - in short all the stuff in the paper that was worth putting a date to. It would be a lot of work, but it would really help to draw the information out of the prose. <br />
Second, a kind of family tree of the languages mentioned in the paper. You see this thing from time to time on the net, but they never have all the little languages mentioned in this paper, like SASL, KRC, Orwell etc. I think that would be a useful contribution to programming language history in general. Again, a lot of work, but worth it in my opinion.<br />
<br />
[[User:DonStewart|dons]] 06:44, 19 July 2006 (UTC) In response to Bernie's comment above regarding timeline, we almost have one. [[Old_news#Archives|This page]], extracted from the mailing list archives 1990-2006. It could possibly be used as a basis for some of the tool releases. <br />
<br />
[[User:DonStewart|dons]] 06:37, 19 July 2006 (UTC) Out of interest, after seeing the mailing list graphs, I've prepared some similar analysis of the [[IRC_channel|#haskell irc channel]]. It too shows similar growth patterns since 2001, when it was created. Details [http://www.cse.unsw.edu.au/~dons/irc/ here]<br />
<br />
[[User:Simonpj|Simonpj]] 11:51, 19 July 2006 (UTC) Interesting data! I didn't know there were 2,000 users of the IRC channel. What does the time axis (labelled 1,2,3 ...) mean? 2001, 2002..? And why does the graph curve down at the end?<br />
<br />
[[User:DonStewart|dons]] 14:15, 19 July 2006 (UTC) The x-axis are the years 2001-2006, (each point is for the previous year), and the graph curves down at the end as 2006-7 isn't finished yet. The 'X' floating above the end of the curve is where we project forwards to the end of the year. Note that we don't ever have 2,000 users concurrently (we averge around 200 users at a time). Over a year, however, 2,000 people (or unique names -- some are duplicates) will visit the channel.<br />
<br />
[[User:Robdockins|Robdockins]] 18:50, 19 July 2006 (UTC) In section 10.3 you mention that the presence of seq damages free theorems and the list deforestation in particular. You might want to mention the following paper, which deals with this issue: http://crab.rutgers.edu/~pjohann/popl04.pdf . Section 8.2 addresses list deforestation in particular.</div>Robdockins