Due: Wednesday, November 22nd, 2023 11:59pm
Difficulty: ★★☆☆
Start with typed_lambda.rhm. The implementation already includes a Boolean type, but no expressions of Boolean type.
Add support for #true, #false, <Exp> == <Exp>, and if <Exp> | <Exp> | <Exp> expressions, where == produces a boolean given two numbers, and if requires a boolean expression for the test. The precedence of == should be just below +, and the precedence of if should be lowest.
Examples:
check: interp(parse('if #true | 4 | 5'),
mt_env)
~is intV(4)
check: interp(parse('if #false | 4 | 5'),
mt_env)
~is intV(5)
check: interp(parse('if 13 == (if 1 == -1 + 2
| 12
| 13)
| 4
| 5'),
mt_env)
~is intV(5)
check: typecheck(parse('13 == (if 1 == -1 + 2
| 12
| 13)'),
mt_env)
~is boolT()
check: typecheck(parse('if 1 == -1 + 2
| fun (x :: Int): x + 1
| fun (y :: Int): y'),
mt_env)
// This result may need to be adjusted after part 3:
~is arrowT(intT(), intT())
check: typecheck(parse('1 + if #true | #true | #false'),
mt_env)
~raises "no type"Implement pair(<Exp>, <Exp>), fst(<Exp>), and snd(<Exp>) expressions with the usual precedence, as well as <Type> * <Type> types where * in types has precedence just above ->. The relevant type rules are shown in video 9. These are eager pairs: pair evaluates its arguments eagerly.
Examples (some of which depend on a choice of constructor and may not apply directly to your implementation):
check: interp(parse('pair(10, 8)'),
mt_env)
// Your constructor might be different than pairV:
~is pairV(intV(10), intV(8))
check: interp(parse('fst(pair(10, 8))'),
mt_env)
~is intV(10)
check: interp(parse('snd(pair(10, 8))'),
mt_env)
~is intV(8)
check: interp(parse('let p :: Int * Int = pair(10, 8):
fst(p)'),
mt_env)
~is intV(10)
check: interp(parse('let f :: Int -> Int * Int
= (fun (n :: Int):
pair(n, n+1)):
snd(f(10))'),
mt_env)
~is intV(11)
check: interp(parse('let f :: Int * Boolean -> Int
= (fun (p :: Int * Boolean):
fst(p)):
f(pair(10, #false))'),
mt_env)
~is intV(10)
check: typecheck(parse('pair(10, 8)'),
mt_env)
// Your constructor might be different than crossT:
~is crossT(intT(), intT())
check: typecheck(parse('fst(pair(10, 8))'),
mt_env)
~is intT()
check: typecheck(parse('snd(pair(10, 8))'),
mt_env)
~is intT()
check: typecheck(parse('let p :: Int * Int = pair(10, 8):
fst(p)'),
mt_env)
~is intT()
check: typecheck(parse('let f :: Int -> Int * Int
= (fun (n :: Int):
pair(n, n+1)):
snd(f(10))'),
mt_env)
~is intT()
check: typecheck(parse('let f :: Int * Boolean -> Int
= (fun (p :: Int * Boolean):
fst(p)):
f(pair(10, #false))'),
mt_env)
~is intT()
check: typecheck(parse('let f :: Int * Boolean -> Boolean
= (fun (p :: Int * Boolean):
snd(p)):
f(pair(10, #false))'),
mt_env)
~is boolT()
check: typecheck(parse('fun (x :: Int * Boolean):
if snd(x)
| fst(x)
| 0'),
mt_env)
// Your constructor might be different than crossT:
~is arrowT(crossT(intT(), boolT()), intT())
check: typecheck(parse('fst(10)'),
mt_env)
~raises "no type"
check: typecheck(parse('1 + fst(pair(#false, 10))'),
mt_env)
~raises "no type"
check: typecheck(parse('fun (x :: Int * Boolean):
if fst(x)
| 1
| 2'),
mt_env)
~raises "no type"With pairs, functions can accept multiple arguments by accepting paired values, but we can also add direct support for multiple arguments.
Change the interpreter to allow multiple function arguments and multiple arguments at function calls. The grammar of the language is now as follows:
<Exp> = <Number>
| #true
| #false
| <Exp> + <Exp>
| <Exp> * <Exp>
| <Exp> == <Exp>
| <Symbol>
| if <Exp> | <Exp> | <Exp>
| fun (<Sym> :: <Type>, ...): <Exp>
| <Exp>(<Exp>, ...)
| let <Sym> :: <Type> = <Exp>: <Exp>
| pair(<Exp>, <Exp>)
| fst(<Exp>)
| snd(<Exp>)
| (<Exp>)
<Type> = Int
| Boolean
| (<Type>, ...) -> <Type>
| <Type> -> <Type>
| <Type> * <Type>
| (<Type>)The <Type> -> <Type> type form is a shorthand for (<Type>) -> <Type> in the case of a single argument. In parse_type, match (<Type>, ...) -> <Type> before <Type> -> <Type>, because a pattern for the latter single-single case will also matche the former multi-argument case.
Examples:
check: interp(parse('(fun (): 10)()'),
mt_env)
~is intV(10)
check: interp(parse('(fun (x :: Int, y :: Int): x+y)(10, 20)'),
mt_env)
~is intV(30)
check: typecheck(parse('(fun (x :: Int, y :: Int): x+y)(10, 20)'),
mt_env)
~is intT()
check: typecheck(parse('(fun (x :: Int, y :: Boolean): y)(10, #false)'),
mt_env)
~is boolT()
check: typecheck(parse('(fun (x :: Int, y :: Boolean): y)(#false, 10)'),
mt_env)
~raises "no type"
check: typecheck(parse('(fun (): 10)(1, 2, 3)'),
mt_env)
~raises "no type"
check: typecheck(parse('let x :: Int = 4:
let f :: (Int, Int) -> Int
= (fun (y :: Int, z :: Int):
z + y):
f(x, x)'),
mt_env)
~is intT()
check: typecheck(parse('let x :: Int = 4:
let f :: (Boolean, Int) -> Int
= (fun (sel :: Boolean, z :: Int):
if sel | x | z):
f(x == 5, 0)'),
mt_env)
~is intT()| Last update: Friday, November 24th, 2023mflatt@cs.utah.edu |