How to use types in Chicken Scheme?

Question

I saw that Chicken scheme has types, but there are no examples in the documentation and I'm not smart enough to deduce the code from the grammar definition in the documentation.

Here is the documentation about types http://wiki.call-cc.org/man/5/Types#type-syntax

I tried this, which I think should not typecheck (fst is defined wrong), but it compiles and executes fine

Here is the code

(: id (forall (a) (a -> a)))
(define id (lambda (a) a))

(: fst (forall (a b) (a b -> a)))
(define (fst a b) b)

(let ()
  (display (fst 1 "oops")))

I build and execute it like this

csc -specialize -strict-types foo.scm && ./foo

Answer 1

The manual suggests that -strict-types may not do what you think it does:

Note that procedure-definitions in dynamically loaded code that was compiled with -strict-types will not check the types of their arguments which will result in unsafe code. Invoking such procedures with incorrectly typed arguments will result in undefined program behaviour.

From experience, the use of type information lends itself to optimization, not enforcement of correctness. Incorrect types may lead to a warning or error, but may as well lead to a crash due to the compiler emitting specialized code that will not work with unexpected data.

This leaves the use of runtime checks and assertions. You may find the simple-contracts egg useful for the former.