A Type System Theory for Higher-Order Intensional Logic Support for Variable Bindings in Hybrid Intensional-Imperative Programs in GIPSY

TL;DR

This paper presents a type system for GIPSY that integrates static and dynamic typing to support intensional programming languages with multidimensional context evaluation.

Contribution

It introduces a novel type system and type theory that unify intensional and imperative languages within GIPSY's compiler and runtime environments.

Findings

Supports multidimensional context evaluation in intensional programming

Ensures type safety across intensional and imperative code

Facilitates execution of various Lucid dialects

Abstract

We describe a type system for a platform called the General Intensional Programming System (GIPSY), designed to support intensional programming languages built upon intensional logic and their imperative counter-parts for the intensional execution model. In GIPSY, the type system glues the static and dynamic typing between intensional and imperative languages in its compiler and run-time environments to support the intensional evaluation of expressions written in various dialects of the intensional programming language Lucid. The intensionality makes expressions to explicitly take into the account a multidimensional context of evaluation with the context being a first-class value that serves a number of applications that need the notion of context to proceed. We describe and discuss the properties of such a type system and the related type theory as well as particularities of the semantics, design and implementation of the GIPSY type system.