Adding Polymorphic Abstraction to ML (Detailed Abstract)

The ML programming language restricts type polymorphism to occur only in the "let-in" construct and requires every occurrence of a formal parameter of a function (a lambda abstraction) to have the same type. Milner in 1978 refers to this restriction (which was adopted to help ML achieve automatic type inference) as a serious limitation. We show that this restriction can be relaxed enough to allow universal polymorphic abstraction without losing automatic type inference. This extension is equivalent to the rank-2 fragment of system F. We precisely characterize the additional program phrases (lambda terms) that can be typed with this extension and we describe typing anomalies both before and after the extension. We discuss how macros may be used to gain some of the power of rank-3 types without losing automatic type inference. We also discuss user-interface problems in how to inform the programmer of the possible types a program phrase may have.

A Biomechanical Model of Human Oculomotor Plant Kinematics Based Upon Geometric Algebra

A biomechanical model of the human oculomotor plant kinematics in 3-D as a function of muscle length changes is presented. It can represent a range of alternative interpretations of the data as a function of one parameter. The model is free from such deficits as singularities and the nesting of axes found in alternative formulations such as the spherical wrist (Paul, l98l). The equations of motion are defined on a quaternion based representation of eye rotations and are compact atnd computationally efficient.