I taught Theory of Computation last Fall and I believe it would be more interesting for students to add some coding implementations. Are you aware of any online course or textbooks in which Haskell (or other languages) are used to teach CS Theory concepts?
This is another not-an-answer that might provide some useful resources. The last is probably the best, but not Haskell related
The two old standards for such a course are:
Introduction to Automata Theory, Languages, and Computation, by Hopcroft, Motwani, and Ullman. Earlier editions were just Hopcroft and Ullman.
Introduction to the Theory of Computation by Sipser.
I don't have the second book, and don't know if it includes any programming exercises, but there might be something in Scheme, knowing Sipser. Amazon's "Look Inside" doesn't seem to work for Sipser.
Two additional books, both very old and hard to get but very highly recommended if you can find them - both short and straightforward with clear explanations are
First Course in Formal Language Theory (Computer science texts) by V. J. Rayward-Smith, and
First Course in Computability (Computer Science Texts) by V. J. Rayward-Smith
The final suggestion is a software system with an associated text.
JFlap was created by Susan Rodger and her colleagues at Duke to form the basis of such a course. Students can easily create all sorts of finite automata. The book they wrote to go with this is JFap: An interactive Formal Languages and Automata Package, Rodger and Finley.
Wikipedia has an overview of JFlap.
Note that JFlap writes automata descriptions in XML which should be easy to parse in any language. All of the automata mentioned in the JFLap tutorial are available for download.
I was part of the NSF evaluation of this system and it is really excellent.
I am not aware of any textbook or online course, no, but I do this myself within my own classroom, and I can share my approach. I use Scheme instead of Haskell, but the method would port quite well to Haskell.
- We spend some time learning a bit about coding in Scheme, and FP in general.
- We cover FSMs and regular expressions, and they code an FSM lab for which they create a
DFAtakes an input string and a machine $(Q, \Sigma, \delta, q_0, F)$ and returns true or false.
NFAtakes an input string, a machine $(Q, \Sigma, \Delta, q_0, F)$, and a maximum number of iterations (to prevent infinite loops), and returns a boolean.
- We cover PDAs and context-free languages, and they create a
PDAlab very similar to
- We go over Turing Machines, and depending on how much time remains in the term, we either do a
TMlab, or if there is not enough time, we do a variant on the Busy Beaver problem where I provide a TM, and their job is to create as many
1s on a tape as possible, with the caveat that the tape must halt by the time the lab is due, and they then submit their machine and a screenshot of the output summary screen. This is done as a contest, and their contest score is $O / (S+A+I)$, where $O$ is the number of $1$s in the final output tape, $S$ is the number of states in the machine, $A$ is the size of the unioned set of input symbols and tape symbols, and $I$ is the number of prewritten states to the tape (i.e. the input). Scores range from .5 to numbers in the quadrillions.
I do more things going forward with untyped $\lambda$ Calculus, and talk a bit about the Church-Turing thesis, but my emphasis switches sufficiently away from computational theory at this point that I wouldn't put it in the same boat any more. We eventually create a REPL and interpreter for untyped lambda calculus (back in Java, no longer in Scheme), that allows for interactions like so:
> 0 = \f.\x.x Added (λf.(λx.x)) as 0 > succ = \n.\f.\x.f (n f x) Added (λn.(λf.(λx.(f ((n f) x))))) as succ > 1 = run succ 0 Added (λf.(λx.(f x))) as 1 > + = λm.λn.λf.λx.(m f) ((n f) x) Added (λm.(λn.(λf.(λx.((m f) ((n f) x)))))) as + > * = λn.λm.λf.λx.n (m f) x Added (λn.(λm.(λf.(λx.((n (m f)) x))))) as * > 2 = run succ 1 Added (λf.(λx.(f (f x)))) as 2 > 3 = run + 2 1 Added (λf.(λx.(f (f (f x))))) as 3 > 4 = run * 2 2 Added (λf.(λx.(f (f (f (f x)))))) as 4 > 5 = + 1 (* 2 2) Added (λf.(λx.(f (f (f (f (f x))))))) as 5 > 7 = run succ (succ 5) Added (λf.(λx.(f (f (f (f (f (f (f x))))))))) as 7 > pred = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u) Added (λn.(λf.(λx.(((n (λg.(λh.(h (g f))))) (λu.x)) (λu.u))))) as pred > 6 = run pred 7 Added (λf.(λx.(f (f (f (f (f (f x1)))))))) as 6 > - = λm.λn.(n pred) m Added (λm.(λn.((n (λn.(λf.(λx.(((n (λg.(λh.(h (g f))))) (λu.x)) (λu.u)))))) m))) as - > 10 = run succ (+ 3 6) Added (λf.(λx.(f (f (f (f (f (f (f (f (f (f x)))))))))))) as 10 > 9 = run pred 10 Added (λf.(λx.(f (f (f (f (f (f (f (f (f x))))))))))) as 9 > 8 = run - 10 2 Added (λf.(λx.(f (f (f (f (f (f (f (f x)))))))))) as 8 > true = λx.λy.x Added (λx.(λy.x)) as true > false = 0 Added (λf.(λx.x)) as false > not = λp.p false true Added (λp.((p (λf.(λx.x))) (λx.(λy.x)))) as not > even? = λn.n not true Added (λn.((n (λp.((p (λf.(λx.x))) (λx.(λy.x))))) (λx.(λy.x)))) as even? > odd? = \x.not (even? x) Added (λx.((λp.((p (λf.(λx.x))) (λx.(λy.x)))) ((λn.((n (λp.((p (λf.(λx.x))) (λx.(λy.x))))) (λx.(λy.x)))) x))) as odd? > run even? 0 true > run even? 5 false
I have much more to say about every one of these things individually, of course, but this answer is only a quick summary of what we do, so I will leave it here for now.