A Type Inference Algorithm For A Linear Lambda Calculus For Hardware Description

Abstract

Based on the close relation between functional languages and hardware circuits, lλ provides a way to specify structural hardware description. Moreover, lλ supports several features of functional languages such as higher-order functions and polymorphism which enable to write programs more succinctly. In spite of these merits, it is impractical to develop a huge circuit with lλ because it requires programmers to annotate all type information

it is a heavy burden onprogrammers, and reduces the code readability. To solve this problem, this paper proposes the algorithm lW (linear W), which is a type inference algorithm for lλ. The algorithm lW, which is based on the algorithmW, automatically finds correct type of any untyped expression. The paper also shows that the algorithm always gives the most general type of any expression.