seunguklee/learning-snupl

Language interpreters and type systems implementation from 4190.310 PL homeworks and lecture notes.

learning-snupl's Issues

Fail polymorphism recursive function test cases (test31, test33)

Test31

• code

let rec f = fn x =>
  f (malloc x); f (write "1"); x
in
  ((f 1) = (f f 1), f f "1")
end

• test result

Expected: (bool , string)
Actual: Type Checking Failed

Test33

• code

let rec f = fn x =>
  (f x) = (f x); malloc (f x); write (f x); x
in
  let val x = "const" in f f x end
end

• test result

Expected: string
Actual: Type Checking Failed

Some test cases failed in polymorphic type checker

Test 16 and Test 20 failed

Test 16

• code

let val print = fn x =>
  (write x; true)
in
  (print 1, (print (fn x => x), print true))
end

• test result

Expected : "Type Checking Failed" 
Actual : (bool , (bool , bool))

Test 20

• code

let val bar = fn x => fn y =>
  if x = y then
    write x
  else
    write y
in
  let val i = 1
      val s = "hello world"
      val b = true
      val l = malloc 10
  in
    (bar i 2, bar s "bye world");
    (fn z => (z, bar (malloc "aa") (malloc "bb"))) (bar b false)
  end
end

• test result

Expected : "Type Checking Failed"
Actual : (bool , loc (string))

Not unusual control-flow problem

• #1 을 fix 하면서 발생한 문제

unify 함수에 pattern matching 에서 다음과 같이 작성하면 문제 없지만:

let rec unify : typ * typ -> Subst.t =
    ...
    fun (given, expected) ->
      match (given, expected) with
      | ...
      | TComparableVar a, t when not (occurs a t) -> ...
      | t, TComparableVar a when not (occurs a t) -> ...
      | TWritableVar a, t when not (occurs a t) -> ...
      | t, TWritableVar a when not (occurs a t) -> ...

다음과 같이 순서가 바뀌어 작성하면 Test 17, 27, 29 가 실패:

let rec unify : typ * typ -> Subst.t =
    ...
    fun (given, expected) ->
      match (given, expected) with
      | ...
      (* Problem *)
      | TWritableVar a, t when not (occurs a t) -> ...
      | t, TWritableVar a when not (occurs a t) -> ...
      | TComparableVar a, t when not (occurs a t) -> ...
      | t, TComparableVar a when not (occurs a t) -> ...