First-class function semantics

First-class function semantics.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Semantics of Dispatcher types and containers of Dispatcher types"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Notation"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Simple types (like integers and floats) will be given names `T`, `T1`, `T2`, ...., `S`, `S1`, `S2`, ...\n",
    "If variable `x` is of type `T` it is written `x: T`.\n",
    "\n",
    "Given types `T1` and `T2`, a function with `T1` as input and `T2` as output is given the type `T1->T2`.\n",
    "\n",
    "To shorten some expressions, function types might be given aliases as `A`, `B`, ...\n",
    "\n",
    "We say that S is a subtype of T, written `S <: T`, to mean that any term of type `S` can safely be used in a context where a term of type `T` is expected.\n",
    "\n",
    "An intersection type is the type of variables that are simultaneously `T1` and `T2` and ... and `Tn`. It's written `x: T1 & T2 & ... & Tn`\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Current situation"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In Numba, dispatchers are their own type. That is, `typeof(foo) == type(CPUDispatcher(<function foo at ...>))`.\n",
    "\n",
    "Certain functions (`cfuncs`, `WAP` wrapping a `CompileResult`, etc) can be assigned a first-class function type, called `FunctionType`.\n",
    "\n",
    "The semantics of this `FunctionType` and associated `UndefinedFunctionType` have never been clarified or documented. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Proposal"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Basic rules\n",
    "- \"Open\" dispatchers (`_can_compile` = True) to continue being their own type, but **Dispatcher types should follow the semantics of intersection types**.\n",
    "- \"Closed\" dispachers with one possible signature to be the same or at least equivalent to FunctionType\n",
    "- \"Closed\" dispatchers with more than one possible signature to be `FunctionIntersectionType`\n",
    "\n",
    "### Consequences\n",
    "- Tuples of open dispatchers to be tuples (not Unituples), of the respective types, as currently.\n",
    "- Typed lists of open dispatchers only allowed via subtyping (see section below)\n",
    "- Tuple of closed dispatchers to be Unituples of the intersection of all `FunctionType` and `FunctionIntersectionType` in the items. If the intersection is empty, this results in a `TypingError`.\n",
    "- Typed lists of closed dispatchers would in principle follow the same rule as tuples, but their mutability adds a type instability problem to their implementation. It should be ok to restrict typed lists of closed dispatchers to those that declare their type in advance.\n",
    "- It is possible that `FunctionIntersectionType` makes `UndefinedFunctionType` unnecessary, but we can only be sure after the implementation is done.\n",
    "    "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Type inference rules\n",
    "\n",
    "Since `Dispatcher` type and `FunctionIntersectionType` are intersection types, it is necessary to clarify their inference rules, which are mostly based on subtyping.\n",
    "\n",
    "The intersection of A & B is identical to the intersection of B & A\n",
    "\n",
    "    A & B == B & A\n",
    "    \n",
    "The intersection of A & B is a subtype of A. That is, if a Dispatcher can be compiled for type A and type B, then it can be used in a context where a function of type A is required, or where a functionof type B is required.\n",
    "\n",
    "    A & B :< A\n",
    "    A & B :< B\n",
    "    \n",
    "The intersection of A & B & C is a subtype of the intersection of A & B and of any 2-combination of A, B and C.\n",
    "\n",
    "    A & B & C :< A & C (and any other 2-combination of A, B, C)\n",
    "    \n",
    "\n",
    "- `Dispatcher` is an intersection type of unknown types, and therefore is not equal to any `FunctionIntersectionType`. Each Dispatcher is a unique type. However, a Dispatcher is a subtype of all function types associated with every supported function signature, and it is a subtype of any `FunctionIntersectionType` formed by subsets of those function types.\n",
    "That is, if DispatcherFoo has n known signatures (but can potentially be compiled for more signatures)\n",
    "\n",
    "`DispatcherFoo : T1 & T2 & .... & Tn & ....`\n",
    "\n",
    "Then,\n",
    "\n",
    "```\n",
    " DispatcherFoo :< T1 \n",
    " DispatcherFoo :< T2\n",
    " ...\n",
    " DispatcherFoo :< Tn\n",
    " DispatcherFoo :< T1 & T2\n",
    " ...\n",
    " DispatcherFoo :< T1 & Tn\n",
    " DispatcherFoo :< T1 & T2 & T3\n",
    " ...\n",
    " DispatcherFoo :< T1 & T2 & Tn\n",
    " ...\n",
    "```\n",
    "\n",
    "### Probing open dispatchers\n",
    "\n",
    "Open dispatchers support a set of known signatures, and also a set of unknown (not yet attempted) signatures.\n",
    "It is an implementation decision whether to attempt compilation for a given signature before deciding if a given dispatcher is a subtype of that signature.\n",
    "\n",
    "### Containers\n",
    "\n",
    "- A tuple of open Dispatchers is a tuple of the individual types.\n",
    "\n",
    "`(Foo1, Foo2, Foo3) : DispacherFoo1 x DispacherFoo2 x DispacherFoo3`\n",
    "\n",
    "- A tuple of open Dispatcher is a subtype of a Unituple of the common signatures, and be cast accordingly.\n",
    "\n",
    "`DispacherFoo1 x DispacherFoo2 x DispacherFoo3 :< A iff every dispatcher supports the signature of type A`\n",
    "\n",
    "`DispacherFoo1 x DispacherFoo2 x DispacherFoo3 :< A & B iff every dispatcher supports the signatures of types A and B`\n",
    "\n",
    "- Tuples of closed dispatchers to be Unituples of the intersection of all supported signatures.\n",
    "\n",
    "`(Foo1, Foo2, Foo3) : Unituple(A, 3) iff A is the only signature supported by all three functions.`\n",
    "\n",
    "`(Foo1, Foo2, Foo3) : Unituple(A&B, 3) iff A and B are the only signatures supported by all three functions.`\n",
    "\n",
    "&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Since these are closed dispatchers, the supported signatures are immediately available at type inference time, and therefore the type of the unituple can be determined.\n",
    "\n",
    "- Given a typed list `List[A]`, any Dispatcher that supports A can be appended to that list. It is an implementation decision whether to attempt compilation of open dispatchers that do not contain known signature A, or to limit the `append` operation to dispatchers for which A is known signature. \n",
    "\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "        \n",
    "        "
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "latest_versions38",
   "language": "python",
   "name": "latest_versions38"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}