15. Choose one of these languages and fill in the gaps to complete the definition.
+<a id="occurs_free"></a>
+
16. Write a function `occurs_free` that has the following type:
occurs_free : identifier -> lambda_term -> bool
-- Or this:
let sysf_true = (\y n -> y) :: Sysf_bool a
- Note that in both OCaml and the Haskell code, the generalization `∀'a` on the free type variable `'a` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
+ Note that in both OCaml and Haskell code, the generalization `∀α` on the free type variable `α` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
:set -XExplicitForAll
let { sysf_true :: forall a. Sysf_bool a; ... }
# k 1 true ;;
- : int = 1
- If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". (WHERE?)
+ If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types".