A constructive proof that Idris is Turing complete.

Turing.idr

%default total

data Direction = L | R

record Machine state halt alphabet where
  constructor MkMachine
  initial : state
  transition : state -> Maybe alphabet -> Maybe (Either halt state, Maybe alphabet, Direction)

data Tape : (a : Type) -> Type where
  Head : List (Maybe a) -> List (Maybe a) -> Tape a

%name Direction dir
%name Machine m
%name Tape tape

empty : Tape a
empty = Head [] []

left : Tape a -> Tape a
left (Head [] right) = Head [] (Nothing :: right)
left (Head (head :: left) right) = Head left (head :: right)

right : Tape a -> Tape a
right (Head left []) = Head (Nothing :: left) []
right (Head left (head :: right)) = Head (head :: left) right

shift : Direction -> Tape a -> Tape a
shift L = left
shift R = right

read : Tape a -> Maybe a
read (Head _ []) = Nothing
read (Head _ (head :: _)) = head

set : Maybe a -> Tape a -> Tape a
set symbol (Head left []) = Head left (symbol :: [])
set symbol (Head left (_ :: right)) = Head left (symbol :: right)

codata Turing : (s, h, a : Type) -> (m : Machine s h a) -> Type where
  Next : s -> Tape a -> Turing s h a m -> Turing s h a m
  Accept : h -> Tape a -> Turing s h a m
  Reject : s -> Tape a -> Turing s h a m

runTuring : Tape a -> (m : Machine s h a) -> Turing s h a m
runTuring input m = go (initial m) input
  where
  go : s -> Tape a -> Turing s h a m
  go state tape =
    let head = read tape in
    case transition m state head of
      Nothing => Reject state tape
      (Just (next, symbol, dir)) =>
        let tape = shift dir (set symbol tape) in
        case next of
          (Left halt) => Accept halt tape
          (Right next) => Next next tape (go next tape)

-- Example

data Q = A | B | C
data H = Halt
_0 : Maybe ()
_0 = Nothing
_1 : Maybe ()
_1 = Just ()

busyBeaver3 : Machine Q H ()
busyBeaver3 = MkMachine A bbStep
  where
  bbStep : Q -> Maybe () -> Maybe (Either H Q, Maybe (), Direction)
  bbStep A Nothing = Just (Right B, _1, R)
  bbStep B Nothing = Just (Right A, _1, L)
  bbStep C Nothing = Just (Right B, _1, L)
  bbStep A (Just ()) = Just (Right C, _1, L)
  bbStep B (Just ()) = Just (Right B, _1, R)
  bbStep C (Just ()) = Just (Left Halt, _1, R)

implementation Show Q where
  show A = "A"
  show B = "B"
  show C = "C"

-- Productive program execution

data RunIO : Type -> Type where
  Quit : a -> RunIO a
  (>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> RunIO a -> IO (Maybe a)
run Dry _ = pure Nothing
run _ (Quit x) = pure (Just x)
run (More fuel) (ctx >>= action) = ctx >>= run fuel . Force . action

printTuring : Turing Q H () Main.busyBeaver3 -> RunIO ()
printTuring (Next state tape cont) = do
  putStrLn ("Step: " ++ show state)
  printTuring cont
printTuring (Accept state tape) = do
  putStrLn "Accept: Halt"
  Quit ()
printTuring (Reject state tape) = do
  putStrLn ("Reject: " ++ show state)
  Quit ()

-- We can happily run any Turing machine, but in the general case, looking at
-- the "entire" answer is uncomputable. (That's the Halting Problem!) You could
-- write a total main here that printed some bounded number of steps, but for
-- convenience, we run forever. Note that only printing it out to the screen is
-- in a partial function, both executing the Turing machine and formatting the
-- execution trace happen in total functions.
partial
main : IO ()
main = run forever (printTuring (runTuring empty busyBeaver3)) *> pure ()
  where
  partial forever : Fuel
  forever = More forever