How can I make type environments for an expression to satisfy specific conditions?

Question

I have a question to make the environment of if true then x else y not closed, closed but not well typed, and closed and well typed. How can I do this in OCaml?

All I know is that not closed means that there is a variable that is not bound. So x and y will not be bound in this case. Additionally, well typed means that the expression satisfies the grammar.

Im not sure how to apply that here however and I only have very wrong answers. Maybe something like:

if (x:int, y:int) then (true) else (false)

if (x:int, y: int) then (x: bool) else (y: bool)

if (true) then (x: int) else (y: int)

for the 3 conditional respectively

Answer 1

You're asking us to do your homework, but we're not taking the class! So we don't have much to go on.

The basic way to bind a variable in OCaml is with let. So if you don't have let x = ... then x is unbound (other things being equal). If you do have something like let x = 4 in ... then x is bound.

Update

Note that (x : int) does not bind x, i.e., it doesn't associate it with a value. It just specifies (or ascribes) the type of x.

Answer 2

It feels like maybe you're coming at this from a Python-esque dynamic viewpoint:

>>> if True:
...   y = 42
... else:
...   x = 27
... 
>>> y
42
>>> x
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'x' is not defined
>>>

OCaml is a statically typed language, where the types of variables are known at compile time. Both x and y have to be bound before you can use them or your program will not compile, much less run. If you need to conditionally bind values to them, you might have a conditional expression return a tuple of values, and use pattern-matching in a let binding:

utop # let (x, y) = if true then (1, 2) else (6, 7);;
val x : int = 1
val y : int = 2

Answer 3

Let's E be your expression if true then x else y.

You can change the environment of E by adding bindings around it:

let x = 0 in E

In which case x is bound in E but y is unbound.

I think the solution you are asked to provide is no more complex than that. The same applies to the other parts of your question.