docs/TypeChecking.ipynb

   1 {
   2  "cells": [
   3   {
   4    "cell_type": "markdown",
   5    "metadata": {},
   6    "source": [
   7     "# Type Checking"
   8    ]
   9   },
  10   {
  11    "cell_type": "code",
  12    "execution_count": 1,
  13    "metadata": {},
  14    "outputs": [],
  15    "source": [
  16     "import logging, sys\n",
  17     "\n",
  18     "logging.basicConfig(\n",
  19     "  format='%(message)s',\n",
  20     "  stream=sys.stdout,\n",
  21     "  level=logging.INFO,\n",
  22     "  )"
  23    ]
  24   },
  25   {
  26    "cell_type": "code",
  27    "execution_count": 2,
  28    "metadata": {},
  29    "outputs": [],
  30    "source": [
  31     "from joy.utils.polytypes import (\n",
  32     "    doc_from_stack_effect, \n",
  33     "    infer,\n",
  34     "    reify,\n",
  35     "    unify,\n",
  36     "    FUNCTIONS,\n",
  37     "    JoyTypeError,\n",
  38     ")"
  39    ]
  40   },
  41   {
  42    "cell_type": "code",
  43    "execution_count": 3,
  44    "metadata": {},
  45    "outputs": [],
  46    "source": [
  47     "D = FUNCTIONS.copy()\n",
  48     "del D['product']\n",
  49     "globals().update(D)"
  50    ]
  51   },
  52   {
  53    "cell_type": "markdown",
  54    "metadata": {},
  55    "source": [
  56     "## An Example"
  57    ]
  58   },
  59   {
  60    "cell_type": "code",
  61    "execution_count": 4,
  62    "metadata": {},
  63    "outputs": [
  64     {
  65      "name": "stdout",
  66      "output_type": "stream",
  67      "text": [
  68       " 25 (--) ∘ pop swap rolldown rrest ccons\n",
  69       " 28 (a1 --) ∘ swap rolldown rrest ccons\n",
  70       " 31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons\n",
  71       " 34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons\n",
  72       " 37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons\n",
  73       " 40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘ \n"
  74      ]
  75     }
  76    ],
  77    "source": [
  78     "fi, fo = infer(pop, swap, rolldown, rrest, ccons)[0]"
  79    ]
  80   },
  81   {
  82    "cell_type": "code",
  83    "execution_count": 5,
  84    "metadata": {},
  85    "outputs": [
  86     {
  87      "name": "stdout",
  88      "output_type": "stream",
  89      "text": [
  90       "([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1])\n"
  91      ]
  92     }
  93    ],
  94    "source": [
  95     "print doc_from_stack_effect(fi, fo)"
  96    ]
  97   },
  98   {
  99    "cell_type": "code",
 100    "execution_count": 6,
 101    "metadata": {},
 102    "outputs": [],
 103    "source": [
 104     "from joy.parser import text_to_expression\n",
 105     "from joy.utils.stack import stack_to_string\n"
 106    ]
 107   },
 108   {
 109    "cell_type": "code",
 110    "execution_count": 7,
 111    "metadata": {},
 112    "outputs": [
 113     {
 114      "name": "stdout",
 115      "output_type": "stream",
 116      "text": [
 117       "[3 4] 2 1 0\n"
 118      ]
 119     }
 120    ],
 121    "source": [
 122     "e = text_to_expression('0 1 2 [3 4]')  # reverse order\n",
 123     "print stack_to_string(e)"
 124    ]
 125   },
 126   {
 127    "cell_type": "code",
 128    "execution_count": 8,
 129    "metadata": {},
 130    "outputs": [
 131     {
 132      "data": {
 133       "text/plain": [
 134        "{a1: 0, a2: 1, a3: 2, a4: 3, a5: 4, s2: (), s1: ()}"
 135       ]
 136      },
 137      "execution_count": 8,
 138      "metadata": {},
 139      "output_type": "execute_result"
 140     }
 141    ],
 142    "source": [
 143     "u = unify(e, fi)[0]\n",
 144     "u"
 145    ]
 146   },
 147   {
 148    "cell_type": "code",
 149    "execution_count": 9,
 150    "metadata": {},
 151    "outputs": [
 152     {
 153      "name": "stdout",
 154      "output_type": "stream",
 155      "text": [
 156       "(... [3 4 ] 2 1 0 -- ... [1 2 ])\n"
 157      ]
 158     }
 159    ],
 160    "source": [
 161     "g = reify(u, (fi, fo))\n",
 162     "print doc_from_stack_effect(*g)"
 163    ]
 164   },
 165   {
 166    "cell_type": "markdown",
 167    "metadata": {},
 168    "source": [
 169     "##  Unification Works \"in Reverse\""
 170    ]
 171   },
 172   {
 173    "cell_type": "code",
 174    "execution_count": 10,
 175    "metadata": {},
 176    "outputs": [],
 177    "source": [
 178     "e = text_to_expression('[2 3]')"
 179    ]
 180   },
 181   {
 182    "cell_type": "code",
 183    "execution_count": 11,
 184    "metadata": {},
 185    "outputs": [
 186     {
 187      "data": {
 188       "text/plain": [
 189        "{a2: 2, a3: 3, s2: (), s1: ()}"
 190       ]
 191      },
 192      "execution_count": 11,
 193      "metadata": {},
 194      "output_type": "execute_result"
 195     }
 196    ],
 197    "source": [
 198     "u = unify(e, fo)[0]  # output side, not input side\n",
 199     "u"
 200    ]
 201   },
 202   {
 203    "cell_type": "code",
 204    "execution_count": 12,
 205    "metadata": {},
 206    "outputs": [
 207     {
 208      "name": "stdout",
 209      "output_type": "stream",
 210      "text": [
 211       "(... [a4 a5 ] 3 2 a1 -- ... [2 3 ])\n"
 212      ]
 213     }
 214    ],
 215    "source": [
 216     "g = reify(u, (fi, fo))\n",
 217     "print doc_from_stack_effect(*g)"
 218    ]
 219   },
 220   {
 221    "cell_type": "markdown",
 222    "metadata": {},
 223    "source": [
 224     "## Failing a Check"
 225    ]
 226   },
 227   {
 228    "cell_type": "code",
 229    "execution_count": 13,
 230    "metadata": {},
 231    "outputs": [
 232     {
 233      "name": "stdout",
 234      "output_type": "stream",
 235      "text": [
 236       " 25 (--) ∘ dup mul\n",
 237       " 28 (a1 -- a1 a1) ∘ mul\n",
 238       " 31 (f1 -- f2) ∘ \n",
 239       " 31 (i1 -- i2) ∘ \n"
 240      ]
 241     }
 242    ],
 243    "source": [
 244     "fi, fo = infer(dup, mul)[0]"
 245    ]
 246   },
 247   {
 248    "cell_type": "code",
 249    "execution_count": 14,
 250    "metadata": {},
 251    "outputs": [
 252     {
 253      "name": "stdout",
 254      "output_type": "stream",
 255      "text": [
 256       "'two'\n"
 257      ]
 258     }
 259    ],
 260    "source": [
 261     "e = text_to_expression('\"two\"')\n",
 262     "print stack_to_string(e)"
 263    ]
 264   },
 265   {
 266    "cell_type": "code",
 267    "execution_count": 15,
 268    "metadata": {},
 269    "outputs": [
 270     {
 271      "name": "stdout",
 272      "output_type": "stream",
 273      "text": [
 274       "Cannot unify 'two' and f1.\n"
 275      ]
 276     }
 277    ],
 278    "source": [
 279     "try:\n",
 280     "    unify(e, fi)\n",
 281     "except JoyTypeError, err:\n",
 282     "    print err"
 283    ]
 284   }
 285  ],
 286  "metadata": {
 287   "kernelspec": {
 288    "display_name": "Python 2",
 289    "language": "python",
 290    "name": "python2"
 291   },
 292   "language_info": {
 293    "codemirror_mode": {
 294     "name": "ipython",
 295     "version": 2
 296    },
 297    "file_extension": ".py",
 298    "mimetype": "text/x-python",
 299    "name": "python",
 300    "nbconvert_exporter": "python",
 301    "pygments_lexer": "ipython2",
 302    "version": "2.7.12"
 303   }
 304  },
 305  "nbformat": 4,
 306  "nbformat_minor": 2
 307 }