Following recent discussions about instance declarations in Haskell-2
on the Haskell mailing list, and the suggestion that without
sufficient restrictions in this area Haskell's type system would
become undecidable, I decided to demonstrate this directly. In this
brief paper I present a construction that encodes a Turing machine
directly in a series of instance declarations. The encoding is such
that it forces the type checker to simulate the operation of a
specified Turing machine in order to check the program. If the Turing
machine terminates then the program is well-typed; if the Turing
machine fails to terminate then it is ill-typed. The well-known
undecidability of the Halting problem thereby carries across to the
unrestricted version of the Haskell-2 type system.
[ An HTML version of this paper, along with the mentioned source
files, appear at
http://www.dcs.gla.ac.uk/~keithw/research/misc/undec.html
An ASCII version of the paper appears below. ]
Instance Declarations are Universal
===================================
Keith Wansbrough
================
July 31, 1998
=============
Following recent discussions about instance declarations in Haskell-2
on the Haskell mailing list, and the suggestion that without
sufficient restrictions in this area Haskell's type system would
become undecidable, I decided to demonstrate this directly. In this
brief paper I present a construction that encodes a Turing machine
directly in a series of instance declarations. The encoding is such
that it forces the type checker to simulate the operation of a
specified Turing machine in order to check the program. If the Turing
machine terminates then the program is well-typed; if the Turing
machine fails to terminate then it is ill-typed. The well-known
undecidability of the Halting problem thereby carries across to the
unrestricted version of the Haskell-2 type system.
A technically superfluous but convenient feature of the encoding is
that a term is provided that, for a well-typed program, yields the
final configuration as a result. It must be stressed that the Turing
machine simulation occurs at type-checking time, even though the final
configuration cannot be inspected until run time. This can easily be
verified by attempting to type check an encoding of a non-terminating
Turing machine.
The undecidability of this type system does not necessarily mean it is
not useful. Indeed, the termination of a Haskell program is also
undecidable, yet Haskell is (therefore??) a useful programming
language. However, undecidability in the type system is unusual and it
is not clear whether or not it is acceptable.
The programs
============
The encoding is performed by a (conventional) Haskell program,
undecgen.lhs. This contains a specification of a Turing machine, and a
generator program. When the function main is invoked, a new literate
Haskell script is generated, containing the encoded representation of
the Turing machine.
The latter script, tmdupl.lhs, must be run under Hugs 1.3c or some
other Haskell environment that supports arbitrary instance contexts
and multiple parameter type classes. When the script is loaded, the
type checker will simulate the Turing machine; if this process
terminates then invoking main will display the final configuration.
The example
===========
The example given is a simple 11-state Turing machine which, given a
string of 1s bounded by a 0 to the left of the head in the initial
position, copies the string (separated by a 0) and leaves the head to
the right of the second copy. For example, it turns 0111[0] into
01110111[0]. The example is adapted from p.188 of Harry Lewis and
Christos Papadimitriou, Elements of the Theory of Computation,
Prentice-Hall, 1981. As noted in the source file, changing a single
rule will convert this machine to a non-terminating one.
Here is a sample run:
1crab % hugs
___ ___ ___ ___ __________ __________
/ / / / / / / / / _______/ / _______/ Hugs 1.4
/ /___/ / / / / / / / _____ / /______
/ ____ / / / / / / / /_ / /______ / The Nottingham and Yale
/ / / / / /___/ / / /___/ / _______/ / Haskell User's System
/__/ /__/ /_________/ /_________/ /_________/ January 1998
Copyright (c) The University of Nottingham and Yale University, 1994-1997.
Bug reports: [EMAIL PROTECTED] Web: http://www.haskell.org/hugs.
Reading file "/local/fp/lib/hugs/1.4-01-1998/hugs/lib/Prelude.hs":
Parsing
Dependency analysis
Type checking
Compiling
Hugs session for:
/local/fp/lib/hugs/1.4-01-1998/hugs/lib/Prelude.hs
Type :? for help
> :l undecgen.lhs
Reading file "undecgen.lhs":
Parsing
Dependency analysis
Type checking
Compiling
Hugs session for:
/local/fp/lib/hugs/1.4-01-1998/hugs/lib/Prelude.hs
undecgen.lhs
> main
> :q
[Leaving Hugs]
2crab % hugs1.3c
__ __ __ __ ____ ___ __________________________________________
|| || || || || || ||__ Hugs 1.3c: The Haskell User's Gofer System
||___|| ||__|| ||__|| __|| Copyright (c) Mark P Jones,
||---|| ___|| The University of Nottingham, 1994-1998.
|| || Report bugs to [EMAIL PROTECTED]
|| || [March 1998] __________________________________________
Reading script file "/users/grad/keithw/lib/hugs1.3c/lib/Prelude.hs":
Parsing
Dependency analysis
Type checking
Compiling
Hugs session for:
/users/grad/keithw/lib/hugs1.3c/lib/Prelude.hs
Type :? for help
? :l tmdupl.lhs
Reading script file "tmdupl.lhs":
Parsing
Dependency analysis
Type checking
Compiling
Hugs session for:
/users/grad/keithw/lib/hugs1.3c/lib/Prelude.hs
tmdupl.lhs
? main
Halted at state Q10. Final configuration is:
(((((((((),S0),S1),S1),S1),S0),S1),S1),S1) <# S0 #> ()
? :q
[Leaving Hugs]
3crab %
After the abovementioned edit, this changes to the following. Notice
how the nontermination shows up at type-checking time, thus confirming
that the type checker is simulating the Turing machine.
1crab % hugs1.3c
__ __ __ __ ____ ___ __________________________________________
|| || || || || || ||__ Hugs 1.3c: The Haskell User's Gofer System
||___|| ||__|| ||__|| __|| Copyright (c) Mark P Jones,
||---|| ___|| The University of Nottingham, 1994-1998.
|| || Report bugs to [EMAIL PROTECTED]
|| || [March 1998] __________________________________________
Reading script file "/users/grad/keithw/lib/hugs1.3c/lib/Prelude.hs":
Parsing
Dependency analysis
Type checking
Compiling
Hugs session for:
/users/grad/keithw/lib/hugs1.3c/lib/Prelude.hs
Type :? for help
? :l tmdupl.lhs
Reading script file "tmdupl.lhs":
Parsing
Dependency analysis
Type checking^C{Interrupted!}
? :q
[Leaving Hugs]
2crab %
The detail
==========
A Turing machine configuration is represented by an instance of a
multiple-parameter type class TM:
> class TM q lss s rss where
> tmfinal :: q -> lss -> s -> rss -> String
Here q is the machine state, lss the left-hand portion of the tape, s
the current symbol, and rss the right-hand portion of the tape. The
method tmfinal returns a string describing the final state of the
Turing machine when started in this configuration.
A machine state is represented by a type Qn containing a single
element of the same name:
> data Q0 = Q0
> data Q1 = Q1
...
> data Q10 = Q10
A tape symbol is represented by a type Sn containing a single element
of the same name. It must be Showable to enable the final
configuration to be displayed.
> data S0 = S0 deriving Show
> data S1 = S1 deriving Show
A portion of tape extending potentially infinitely in one direction is
represented by a series of nested pairs. For the left-hand portion,
the tape is either () (unit) representing all S0s, or a pair (lss,ls)
representing the tape lss followed by the symbol ls. The right-hand
portion is similar but the pair is swapped: (rs,rss).
A transition begins with a comment describing it, followed by the
instance declarations. The head of the instance declaration is the
initial state, and the context is the final state; note that this
gives the instance declaration a counterintuitive direction. The
method declaration of tmfinal, however, is in the expected order.
==> (Q0,S0)->(L,Q1):
> instance TM Q1 lss ls (S0,rss) => TM Q0 (lss,ls) S0 rss where
> tmfinal Q0 (lss,ls) S0 rss = tmfinal Q1 lss ls (S0,rss)
> instance TM Q1 () S0 (S0,rss) => TM Q0 () S0 rss where
> tmfinal Q0 () S0 rss = tmfinal Q1 () S0 (S0,rss)
The first instance declaration gives the rule in the general case; the
second gives the rule to extend the tape when necessary. Note that
these do not overlap; in fact, this implementation does not require
overlapping instances at all.
A halting `transition' looks slightly different:
==> (Q10,S0)->(HALT,Q10):
> instance (Show lss, Show rss) => TM Q10 lss S0 rss where
> tmfinal Q10 lss S0 rss = "Halted at state Q10. "
> ++ "Final configuration is:\n"
> ++ show lss ++ " <# "
> ++ show S0 ++ " #> " ++ show rss
Here there is no final state for the transition, and hence the
instance context does not contain a machine state. Instead, we need to
be able to display the final configuration in tmfinal, so we require
the tapes to be Showable. They will be, since individual symbols are
and the rule for pairs is built in.
Finally, an initial state is given to the type checker in the
declaration of main:
> main :: IO ()
> main = putStr (tmfinal Q0 ((((),S1),S1),S1) S0 ())
How it works
============
The operation is fairly simple. We start by trying to type an initial
configuration: since we use tmfinal at a particular set of types, we
need to find the appropriate instance declaration. The type checker
matches the initial configuration against the head of the appropriate
declaration, but then discovers that the context requires another
configuration. It searches for this, and matches against the
appropriate head. This causes another transition; and so on.
If eventually we meet a configuration with a context we can resolve
(i.e., a halting configuration), the process terminates and the type
checker has proven the program well-typed (i.e., that the TM
halts). Then at run time, the invocation of tmfinal eventually invokes
the appropriate code in the halting configuration and displays the
final configuration as desired.
We cannot distinguish, however, between a (machine,instance) pair that
simply runs for a long time and a pair that never
terminates. Obviously in certain limited cases it is possible, but the
familiar diagonalisation argument shows it is not possible in
general. Either we restrict the set of acceptable instance
declarations until only terminating (machine,instance) pairs are
permitted (but thereby rule out many perfectly valid types along with
the invalid ones); or we live with the fact that some types may cause
the type checker to fail to terminate, rather than yielding an error.
Keith Wansbrough, July 31, 1998
--KW 8-)
--
: Keith Wansbrough, MSc, BSc(Hons) (Auckland) -------------------------:
: PhD Student, Computing Science, University of Glasgow, Scotland. :
: Native of Antipodean Auckland, New Zealand: 174d47' E, 36d55' S. :
: http://www.dcs.gla.ac.uk/~keithw/ mailto:[EMAIL PROTECTED] :
:----------------------------------------------------------------------:
