Graphical type inference: A graph grammar definition

Abstract

We present a graph grammar based type inference system for a totally graphic language inspired in the data flow view of lazy functional programs. NiMo (Nets in Motion) can be seen as a graphic equivalent to Haskell that acts as an on-line tracer and debugger. The user not only sees the results but also the way they are calculated according to an understandable model and can interrupt the execution at any point, change data, processes and/or process activation, undo steps, and also execute incomplete programs. Type inference is incremental; during the net edition (construction or modification) only type safe connections are allowed. The user visualises the type information evolution and, in case of type error, can identify where and why it happened. The NiMo type system, though similar, has significant differences with systems in functional languages due to the data flow ingredient. It needs to cope with processes with no entries and zero or more that one output and therefore the process type is a generalization of functional types. We present the notion of non-structural type unification, the elements for modelling graphic type inference, and the correspondence with the classical type inference approach. Construction and execution of NiMo programs are fully defined via an attributed graph grammar. In the previous version type information was incomplete and static type inference was partial in presence of polymorphism. Therefore type inconsistent nets could be executed. Here we present the type descriptor graphs and the graph grammar definition of the complete static type inference system. The grammar has been implemented and successfully tested using AGG as the graph transformation system.