The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

If we view Coq as a programming language with

(1) dependant types
(2) terminating functions
(3) Haskell, Scheme and Ocaml as its `assembler language'

but without input and output. What is the best (or a good) way to model
input and output in Coq?

The IO monad of Haskell looks like an good starting point, but it does
not work:
---------------------------------------
Parameter IO : Set -> Set.
Parameter io_bind : forall A B:Set, IO A -> (A -> IO B) -> IO B.
Parameter io_return : forall A:Set, A -> IO A.
Definition test := return nat O.

Extraction Language Haskell.
Extract Constant IO "a" => "IO".
Extract Constant io_bind => "(>>=)".
Extract Constant io_return => "return".
Extraction "World"
   IO io_bind io_return
   test
.

==> The file World.hs has been created by extraction.
---------------------------------------

But World.hs contains:
---------------------------------------
module World where

import qualified Prelude

data Nat = O
           | S Nat

type IO x = () -- AXIOM TO BE REALIZED


io_bind =
  Prelude.error "AXIOM TO BE REALIZED"

io_return =
  Prelude.error "AXIOM TO BE REALIZED"

test =
  io_return O

--------------------------------------

Some ideas:
(a) The unique World approach of Clean.
(b) Encode open file descriptors etc. in a dependant type.
(c) An imperative style.

I'm using:
The Coq Proof Assistant, version 8.0 (Apr 2004)
compiled on Jun 11 2004 16:28:34

Sincerly,
-- 
Stefan