Type error checker for type-free or polymorphic computer language

• US 5,748,966 A
• Filed: 12/30/1994
• Issued: 05/05/1998
• Est. Priority Date: 12/30/1994
• Status: Expired due to Term

• Current Assignee: Trustees Of The University Of Pennsylvania (University of Pennsylvania)
• Original Assignee: Trustees Of The University Of Pennsylvania (University of Pennsylvania)
• Inventors: Sato, Yoshikazu
• Primary Examiner(s): Oberley, Alvin E.
• Assistant Examiner(s): CORCORAN, PETER JOSEPH
• Application Number:
  US08/366,894
• Time in Patent Office: 1,222 Days
• Field of Search: 395/700, 395/701, 395/703, 395/704, 395/705, 395/707, 395/708, 395/650, 364/DIG. 1
• US Class Current: 717/131
• CPC Class Codes: G06F 8/437 Type checking

Abstract

A system and method for a run-time type error in a program prior to running the program whose source code is written in a programming language with imperative constructs and polymorphic procedures is disclosed. To accomplish the above type error checking, the source code is translated into intermediate form representations by an intermediate form translator. In addition to the intermediate form representations, type representations which include predetermined types such as a locking type constructor and an unlocking type constructor are utilized in detecting the run-time type error. When both intermediate form representations and the type representations are used and the source code is determined to have no run-time type error prior to running the program according to the current invention, it is guaranteed that the program will run without any run-time type error.

Claims

1. A system for detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising:

an intermediate form translator for translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations;

type representations having predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for defining predetermined locked types so as to ultimately prevent run-time type errors associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types; and

a type checker in response to said intermediate form representations and the type representations for checking whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error, said exact type excluding a type equal to and more general than said predetermined locked types.

2. The system for type checking according to claim 1 wherein said programming language includes at least ML and LISP.

3. The system for type checking according to claim 2 wherein said polymorphic procedures in said ML are used at least with any combination of constants, term variables, lambda-expressions, function applications and let expressions.

4. The system for type checking according to claim 1 wherein said mutuality includes a jumping operation with a value passing and a referencing operation.

5. The system for type checking according to claim 4 wherein said referencing operation further includes reference creation, dereferencing and assignment.

6. The system for type checking according to claim 1 wherein said predetermined types further include at least a base type, a type variable, a function type, and a reference type.

7. The system for type checking according to claim 6 wherein said intermediate form representations include expressions, said expressions further including sub-expressions.

8. The system for type checking according to claim 6 wherein said type checker determines a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types.

9. The system for type checking according to claim 8 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being unlocked upon a detection of reference to said mutual object resulting in an unlocked type.

10. The system for type checking according to claim 9 wherein said mutual object includes a reference cell and a passing value for jumping to a predetermined location.

11. The system for type checking according to claim 9 wherein said reference includes dereferencing and a use of said passing value in said predetermined location.

12. The system for type checking according to claim 9 wherein said run-time type error being suspected when said type variable in said locked type defining a locked type variable is substituted with a specific type before resulting in said unlocked type.

13. The system for type checking according to claim 12 wherein said program is free of said run-time type error when none of said locked type variables is substituted with said specific type before resulting in said unlocked type.

14. The system for type checking according to claim 13 wherein said specific type excludes a type equal to and more general than said locked type variable.

15. The system for type checking according to claim 7 wherein said type checker further comparing:

a first type checker in response to said intermediate form representations and said type representations for determining a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types; and

a second type checker in response to said intermediate form representations and said type representations for further determining if said expression will be free of said run-time type error.

16. The system for type checking according to claim 15 wherein said first type checker generates a symbol table including local variables and corresponding types.

17. The system for type checking according to claim 15 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being marked for unlocking upon a detection of reference to said mutual object.

18. The system for type checking according to claim 17 wherein said type variable in said locked type defines a locked type variable.

19. The system for type checking according to claim 18 wherein said first type checker determines a substitution for substituting said locked type variable of a binding expression of said let expression to a specific type, defining at least a part of a let expression typing rule.

20. The system for type checking according to claim 19 wherein said second type checker in response to said substitution in said first type checker further determines a first type of a local variable of said let expression and then a second type of a body of said let expression based upon said first type indicating that said let expression is free of said run-time type error.

21. The system for type checking according to claim 20 wherein said let expression typing rule further includes a fork operation and a close operation, a non-locked type variable consisting of none-locked occurrence of a partially locked type variable and not-locked type variable.

22. The system for type checking according to claim 21 wherein said fork operation replaces each of nonlocked occurrences of said type variables with a fresh type variable except for said non-locked type variable appearing in said symbol table.

23. The system for type checking according to claim 22 wherein said close operation lists said type variables that may be used for substituting to a specific type, said listed type variables excluding said non-locked type variable appearing in said symbol table, and locked type variables and locked occurrences of partially locked type variables in said first type of said local variable.

24. The system for type checking according to claim 23 wherein said close operation associates said type variable with said symbol table defining an associated locked type variable if said type variable is not yet associated, fully locked in said first type of said local variable and fully locked or not appearing in said symbol table.

25. The system for type checking according to claim 24 wherein said type variable has a priority for unification in relation a second type variable based upon said symbol table.

26. The system for type checking according to claim 25 wherein said second type checker returns said second type of said expression if none of said run-time type error is detected.

27. The system for type checking according to claim 26 wherein upon a detection of said unlocking constructor at the outer most position in said sub-expression'"'"'s type, defining an unlocking typing rule.

28. The system for type checking according to claim 27 wherein said unlocking typing rule further includes an unlock operation, an Ufork operation and said close operation.

29. The system for type checking according to claim 28 wherein said unlock operation unlocks said marked type which results in an unlocked type.

30. The system for type checking according to claim 28 wherein said Ufork operation replaces each of said non-locked type variable that is associated with said symbol table with a fresh type variable.

31. The system for type checking according to claim 25 wherein said associated locked type variable is substituted to said second type variable when said second type variable appears in said symbol table, said unification is defined to be successfully completed.

32. The system for type checking according to claim 25 wherein said second type variable is substituted to said associated locked type variable when said symbol table lacks said second type variable, said unification is defined to be successfully completed.

33. A method of detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising the steps of:

a. providing type representations hating predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for preventing run-time type error associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types;

b. translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations; and

c. determining in response to said intermediate form representations and said type representations whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error.

34. The method of type checking according to claim 33 wherein said programming language includes at least ML and LISP.

35. The method of type checking according to claim 34 wherein said polymorphic procedures in said ML are used at least with any combination of constants, term variables, lambda-expressions, function applications and let expressions.

36. The method of type checking according to claim 33 wherein said step c determines whether mutuality in relation to said imperative constricts in said program will be free of said run-time type error.

37. The method of type checking according to claim 36 wherein said mutuality includes a jumping operation with a value passing and a referencing operation.

38. The method of type checking according to claim 37 wherein said referencing operation further includes reference creation, dereferencing and assignment.

39. The method of type checking according to claim 33 wherein said predetermined types further include at least a base type, a type variable, a function type, and a reference type.

40. The method of type checking according to claim 39 wherein said intermediate form representations include expressions, said expressions further including sub-expressions.

41. The method of type checking according to claim 40 wherein said step c determines a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types.

42. The method of type checking according to claim 41 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being unlocked upon a detection of reference to said mutual object resulting in an unlocked type.

43. The method of type checking according to claim 42 wherein said mutual object includes a reference cell and a passing value for jumping to a predetermined location.

44. The method of type checking according to claim 42 wherein said reference includes dereferencing and a use of said passing value in said predetermined location.

45. The method of type checking according to claim 42 wherein said run-time type error being suspected when said type variable in said locked type defining a locked type variable is substituted with a specific type before resulting in said unlocked type.

46. The method of type checking according to claim 45 wherein said program is free of said run-time type error when none of said locked type variables is substituted with said specific type before resulting in said unlocked type.

47. The method of type checking according to claim 46 wherein said specific type excludes a type equal to and more general than said locked type variable.

48. The method of type checking according to claim 40 wherein said step c further comprises the steps of:

d. determining a first type for each of said sub-expressions in response to said intermediate form representations and said type representations and then a second type for said expression based upon a plurality of said first types; and

e. further determining in response to said intermediate form representations and said type representations whether if said expression will be free of said run-time type error.

49. The method of type checking according to claim 48 wherein said step d generates a symbol table including local variables and corresponding types.

50. The method of type checking according to claim 48 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being marked for unlocking upon a detection of reference to said mutual object.

51. The method of type checking according to claim 50 wherein said type variable in said locked type defines a locked type variable.

52. The method of type checking according to claim 51 wherein said step d determines a substitution for substituting said locked type variable of a binding expression of said let expression to a specific type, defining at least a part of a let expression typing rule.

53. The method of type checking according to claim 52 wherein said step e in response to said substitution in said first type checker further determines a first type of a local variable of said let expression and then a second type of a body of said let expression based upon said first type indicating that said let expression is free of said run-time type error.

54. The method of type checking according to claim 53 wherein said let expression typing rule further includes a fork operation and a close operation, a non-locked type variable consisting of none-locked occurrence of a partially locked type variable and not-locked type variable.

55. The method of type checking according to claim 54 wherein said fork operation replaces each of nonlocked occurrences of said type variables with a fresh type variable except for said non-locked type variable appearing in said symbol table.

56. The method of type checking according to claim 55 wherein said close operation lists said type variables that may be used for substituting to a specific type, said listed type variables excluding said non-locked type variable appearing in said symbol table, and locked type variables and locked occurrences of partially locked type variables in said first type of said local variable.

57. The method of type checking according to claim 56 wherein said close operation associates said type variable with said symbol table defining an associated locked type variable if said type variable is not yet associated, fully locked in said first type of said local variable and fully locked or not appearing in said symbol table.

58. The method of type checking according to claim 57 wherein said type variable has a priority for unification in relation a second type variable based upon said symbol table.

59. The method of type checking according to claim 58 wherein said step e returns said second type of said expression if none of said run-time type error is detected.

60. The method of type checking according to claim 59 wherein upon a detection of said unlocking constractor at the outer most position in said sub-expression'"'"'s type, defining an unlocking typing rule.

61. The method of type checking according to claim 60 wherein said unlocking typing rule further includes an unlock operation, an Ufork operation and said close operation.

62. The method of type checking according to claim 61 wherein said unlock operation unlocks said marked type which results in an unlocked type.

63. The method of type checking according to claim 61 wherein said Ufork operation replaces each of said non-locked type variable that is associated with said symbol table with a fresh type variable.

64. The method of type checking according to claim 58 wherein said associated locked type variable is substituted to said second type variable when said second type variable appears in said symbol table, said unification is defined to be successfully completed.

65. The method of type checking according to claim 58 wherein said second type variable is substituted to said associated locked type variable when said symbol table lacks said second type variable, said unification is defined to be successfully completed.