Browse Source

Initial commit

Amélia Liao 7 years ago
commit
1b87d2cde7
91 changed files with 14974 additions and 0 deletions
  1. +13
    -0
      .gitignore
  2. +25
    -0
      blag.cabal
  3. +45
    -0
      css/code.css
  4. +13
    -0
      css/computermodern.css
  5. +469
    -0
      css/default.scss
  6. +1
    -0
      css/katex.min.css
  7. +15
    -0
      diagrams/cc/delimcc.tex
  8. +1
    -0
      diagrams/eq/0cube.tex
  9. +4
    -0
      diagrams/eq/1cube.tex
  10. +6
    -0
      diagrams/eq/2cube.tex
  11. +5
    -0
      diagrams/eq/interval.tex
  12. +39
    -0
      diagrams/gm/app_gx.tex
  13. +51
    -0
      diagrams/gm/app_kgx.tex
  14. +25
    -0
      diagrams/gm/entry.tex
  15. +31
    -0
      diagrams/gm/push_g.tex
  16. +44
    -0
      diagrams/gm/push_k.tex
  17. +33
    -0
      diagrams/gm/push_x.tex
  18. +34
    -0
      diagrams/gm/slide_3.tex
  19. +25
    -0
      diagrams/gm/spine+stack.tex
  20. +14
    -0
      diagrams/gm/spine.tex
  21. +1
    -0
      diagrams/template/step1.tex
  22. +26
    -0
      diagrams/template/step2.tex
  23. +33
    -0
      diagrams/template/step3.tex
  24. +38
    -0
      diagrams/template/step4.tex
  25. +38
    -0
      diagrams/template/step4red.tex
  26. +22
    -0
      diagrams/template/step5.tex
  27. +2
    -0
      hie.yaml
  28. +140
    -0
      package-lock.json
  29. +21
    -0
      package.json
  30. +35
    -0
      pages/contact.md
  31. +13
    -0
      pages/index.html
  32. +14
    -0
      pages/oss.md
  33. +308
    -0
      pages/posts/2016-08-17-parsec.md
  34. +331
    -0
      pages/posts/2016-08-23-hasochism.lhs
  35. +172
    -0
      pages/posts/2016-08-26-parsec2.lhs
  36. +155
    -0
      pages/posts/2017-08-01-delimcc.md
  37. +231
    -0
      pages/posts/2017-08-02-urnmatch.md
  38. +276
    -0
      pages/posts/2017-08-06-constraintprop.md
  39. +280
    -0
      pages/posts/2017-08-15-multimethods.md
  40. +516
    -0
      pages/posts/2017-09-08-dependent-types.md
  41. +456
    -0
      pages/posts/2018-01-18-amulet.md
  42. +609
    -0
      pages/posts/2018-02-18-amulet-tc2.md
  43. +286
    -0
      pages/posts/2018-03-14-amulet-safety.md
  44. +247
    -0
      pages/posts/2018-03-27-amulet-gadts.md
  45. +304
    -0
      pages/posts/2018-08-11-amulet-updates.md
  46. +329
    -0
      pages/posts/2019-01-28-mldelta.lhs
  47. +191
    -0
      pages/posts/2019-09-22-amulet-records.md
  48. +136
    -0
      pages/posts/2019-09-25-amc-prove.md
  49. +202
    -0
      pages/posts/2019-09-29-amc-prove-interactive.md
  50. +369
    -0
      pages/posts/2019-10-04-amulet-kinds.md
  51. +126
    -0
      pages/posts/2019-10-19-amulet-quicklook.md
  52. +1355
    -0
      pages/posts/2020-01-31-lazy-eval.lhs
  53. +380
    -0
      pages/posts/2020-07-12-continuations.md
  54. +162
    -0
      pages/posts/2020-09-09-typing-proof.md
  55. +264
    -0
      pages/posts/2020-10-30-reflecting-equality.md
  56. +637
    -0
      pages/posts/2021-01-15-induction.md
  57. +321
    -0
      site.hs
  58. +6
    -0
      stack.yaml
  59. +33
    -0
      stack.yaml.lock
  60. +140
    -0
      static/Parser.hs
  61. +239
    -0
      static/Parser.hs.html
  62. +10
    -0
      static/default.css
  63. +100
    -0
      static/demorgan-1.ml.html
  64. +3024
    -0
      static/doom.svg
  65. +119
    -0
      static/forth_machine.js
  66. +22
    -0
      static/generated_code.lua
  67. +124
    -0
      static/generated_code.lua.html
  68. BIN
      static/icon/android-chrome-192x192.png
  69. BIN
      static/icon/android-chrome-512x512.png
  70. BIN
      static/icon/apple-touch-icon.png
  71. BIN
      static/icon/favicon-16x16.png
  72. BIN
      static/icon/favicon-32x32.png
  73. BIN
      static/icon/favicon.ico
  74. BIN
      static/icon/valid-html20.png
  75. +93
    -0
      static/licenses/LICENSE.FantasqueSansMono
  76. +21
    -0
      static/licenses/LICENSE.KaTeX
  77. BIN
      static/pfp.jpg
  78. +215
    -0
      static/profunctor-impredicative.ml.html
  79. +224
    -0
      static/profunctors.ml.html
  80. +26
    -0
      static/tasks.lisp
  81. +126
    -0
      static/tasks.lisp.html
  82. BIN
      static/verify_error.png
  83. BIN
      static/verify_warn.png
  84. +8
    -0
      sync
  85. +190
    -0
      syntax/amcprove.xml
  86. +222
    -0
      syntax/amulet.xml
  87. +2
    -0
      templates/archive.html
  88. +71
    -0
      templates/default.html
  89. +10
    -0
      templates/post-list.html
  90. +10
    -0
      templates/post.html
  91. +20
    -0
      templates/tikz.tex

+ 13
- 0
.gitignore View File

@ -0,0 +1,13 @@
/.site
/.store
/.stack-work
/.vscode
/node_modules
/uni
/portfolio.md
/fonts
/css/fonts
/.mailmap

+ 25
- 0
blag.cabal View File

@ -0,0 +1,25 @@
name: blag
version: 0.1.0.0
build-type: Simple
cabal-version: >= 1.10
executable site
main-is: site.hs
build-depends: base
, hakyll
, pandoc
, skylighting
, process
, containers
, directory
, pandoc-types
, bytestring
, uri-encode
, deepseq
, text
, hsass
, hakyll-sass
ghc-options: -threaded
default-language: Haskell2010
ghc-options: -optl-fuse-ld=lld

+ 45
- 0
css/code.css View File

@ -0,0 +1,45 @@
code, div.sourceCode {
font-family: Fantasque Sans Mono, Fira Mono, monospace;
font-size: 15pt;
}
code.inline {
background-color: rgb(250,250,250);
/* border: 1px solid rgb(200,200,200); */
}
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode {
margin: 0; padding: 0; vertical-align: baseline; border: none;
}
table.sourceCode {
width: 100%; line-height: 100%;
}
td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; }
td.sourceCode { padding-left: 5px; }
code.kw, span.kw { color: #af005f; } /* Keyword */
code.dt, span.dt { color: #5f5faf; } /* DataType */
code.dv, span.dv { color: #268bd2; } /* DecVal */
code.bn, span.bn { color: #268bd2; } /* BaseN */
code.fl, span.fl { color: #268bd2; } /* Float */
code.ch, span.ch { color: #cb4b16; } /* Char */
code.st, span.st { color: #cb4b16; } /* String */
code.co, span.co { color: #8a8a8a; } /* Comment */
code.ot, span.ot { color: #007020; } /* Other */
code.al, span.al { color: #ff0000; } /* Alert */
code.fu, span.fu { color: #666666; } /* Function */
code.er, span.er { color: #ff0000; } /* Error */
code.wa, span.wa { color: #60a0b0; } /* Warning */
code.cn, span.cn { color: #880000; } /* Constant */
code.sc, span.sc { color: #4070a0; } /* SpecialChar */
code.vs, span.vs { color: #4070a0; } /* VerbatimString */
code.ss, span.ss { color: #2aa198; } /* SpecialString */
code.va, span.va { color: #073642; } /* Variable */
code.cf, span.cf { color: #007020; } /* ControlFlow */
code.op, span.op { color: #d33682; } /* Operator */
code.pp, span.pp { color: #bc7a00; } /* Preprocessor */
code.at, span.at { color: #7d9029; } /* Attribute */
code.do, span.do { color: #ba2121; } /* Documentation */
code.an, span.an { color: #60a0b0; } /* Annotation */
code.cv, span.cv { color: #60a0b0; } /* CommentVar */

+ 13
- 0
css/computermodern.css View File

@ -0,0 +1,13 @@
@font-face {
font-family: "Computer Modern";
src: url('/static/cmunorm.woff');
}
.math {
font-family: Computer Modern, serif;
}
.math .display {
font-size: 18px;
text-align: center;
}

+ 469
- 0
css/default.scss View File

@ -0,0 +1,469 @@
$purple: #424969;
$orange: #ffac5f;
$blonde: #f5ddbc;
$light-purple: #faf0fa;
$yugo: #ea8472;
$header: $orange;
$header-height: 50px;
$max-width: 95ch;
.mathpar, .math-paragraph {
display: flex;
flex-direction: row;
flex-wrap: wrap;
justify-content: space-around;
align-items: center;
}
a#mastodon {
display: none;
}
html, body {
min-height: 100%;
height: 100%;
margin: 0;
background-color: white;
font-family: -apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Oxygen-Sans,Ubuntu,Cantarell,"Helvetica Neue",sans-serif;
}
body {
display: flex;
flex-direction: column;
counter-reset: theorem figure;
}
div#header {
background-color: $header;
height: $header-height;
display: flex;
flex-direction: row;
align-items: stretch;
justify-content: space-between;
flex-wrap: nowrap;
overflow-x: auto;
div#logo {
margin-left: .5em;
line-height: $header-height;
padding-left: .5em;
padding-right: .5em;
font-size: 18pt;
a {
color: $purple;
text-decoration: none;
}
transition: background-color .2s ease-in-out;
}
div#logo:hover {
background-color: darken($header, 10%);
}
div#navigation {
margin-right: .5em;
display: flex;
flex-direction: row;
align-items: stretch;
align-self: flex-end;
justify-content: flex-end;
line-height: $header-height;
a {
color: $purple;
text-decoration: none;
margin-left: .5em;
margin-right: .5em;
}
div.nav-button {
height: 100%;
transition: background-color .2s ease-in-out;
}
div.nav-button:hover {
background-color: darken($header, 10%);
}
}
}
div#content {
max-width: $max-width;
margin: 0px auto 0px auto;
flex: 1 0 auto;
span.katex, span.together {
display: inline-block;
}
p {
text-align: justify;
letter-spacing: 1.75;
code {
display: inline-block;
}
span.qed {
float: right;
}
span.theorem ::after {
counter-increment: theorem;
content: " " counter(theorem);
}
span.theorem, span.paragraph-marker {
font-style: italic;
}
}
p.image {
text-align: center !important;
}
h1 {
font-variant: small-caps;
max-width: 120ch;
}
blockquote {
background-color: $light-purple;
border-radius: 10px;
border: 1px solid $purple;
padding: 0em 1em;
}
> article > blockquote {
width: 80%;
margin: auto;
}
> article > div.code-container {
width: 80%;
margin: auto;
pre {
padding: 0px 1em;
}
> span {
display: inline;
}
}
div.code-container {
background-color: $light-purple;
border-radius: 10px;
border: 1px solid darken($light-purple, 10%);
overflow-x: auto;
> span {
padding: 0.5em 1em 0.25em 1em;
background-color: darken($light-purple, 10%);
border-top-left-radius: 10px;
box-shadow: 1px 1px darken($light-purple, 20%);
display: none;
}
> span::after {
content: " code";
}
div.sourceCode {
padding: 0px .5em;
}
}
div.code-container.custom-tag {
> span::after {
display: none;
}
}
div.code-container.continues {
> span {
display: none;
}
}
* {
max-width: 100%;
}
details {
summary {
margin-left: 1em;
font-size: 14pt;
padding: .2em 1em;
}
border-radius: 5px;
border: 1px solid $purple;
padding: .2em 1em;
background-color: white;
font-size: 0pt;
margin-top: 0.5em;
margin-bottom: 0.5em;
transition: font-size 0.3s ease-in-out, background-color 0.3s ease-in-out;
transform: rotate3d(0, 0, 0, 0);
}
details[open] {
background-color: $light-purple;
font-size: 14pt;
}
.special-thanks {
display: flex;
flex-direction: column;
align-items: center;
justify-content: space-around;
p {
font-size: 21pt;
margin-top: .5em;
margin-bottom: 0px;
}
ul {
list-style: none;
li {
margin: .5em 0px;
border-radius: 10px;
border: 1px solid $purple;
background-color: $light-purple;
padding: 1em;
a {
text-decoration: underline;
}
transition: all 0.2s ease-in-out;
}
li:hover {
border-radius: 5px;
transform: scale(1.01);
background-color: lighten($light-purple, 5%);
}
}
}
.eqn-list {
list-style: none;
direction: rtl;
counter-reset: equation;
li {
counter-increment: equation;
span.katex-display {
margin: 2px;
}
* {
direction: ltr;
}
}
li::marker {
content: "(" counter(equation) ")";
font-family: KaTeX_Main, Times New Roman, serif;
}
}
font-size: 14pt;
line-height: 1.6;
}
div.info, span#reading-length {
padding-left: 1em;
font-style: italic;
}
span#reading-length::before {
content: "Word count: "
}
div#footer {
display: flex;
align-items: center;
justify-content: space-between;
padding-left: 1em;
padding-right: 1em;
background-color: $light-purple;
}
.definition {
text-decoration: dotted underline;
}
.post-list {
list-style: none;
padding: 0px;
div.post-list-item {
margin-top: .2em;
margin-bottom: .2em;
padding: 1em;
border-radius: 10px;
background-color: $light-purple;
display: flex;
justify-content: space-between;
flex-wrap: wrap;
align-items: flex-end;
font-size: 11pt;
a {
font-size: 14pt;
padding-right: 2em;
}
}
}
table {
margin: auto;
border-collapse: collapse;
td, th {
border: 1px solid $purple;
text-align: center;
padding: 0px 1em 0px 1em;
> * {
vertical-align: middle;
}
}
td.image {
padding: 0px;
img {
margin-top: auto;
}
}
}
figure {
width: 100%;
margin: auto;
display: flex;
flex-direction: column;
align-items: center;
justify-content: space-around;
div {
width: 100%;
overflow-x: auto;
}
figcaption {
font-size: 14pt;
}
figcaption::before {
counter-increment: figure;
content: "Figure " counter(figure) ". ";
}
}
@media only screen and (max-width: $max-width) {
div#content {
margin-left: 1em;
margin-right: 1em;
}
.mathpar {
overflow-x: auto;
justify-content: space-evenly;
> * {
margin-left: .2em;
margin-right: .2em;
flex-shrink: 0;
flex-grow: 0;
}
}
}
// Contact page
.contact-list {
display: flex;
flex-direction: row;
flex-wrap: wrap;
justify-content: space-around;
align-items: center;
.contact-card {
margin: 0px .5em;
border: 1px solid $purple;
border-radius: 10px;
background-color: $blonde;
padding: 0px 1em;
.username, .username * {
font-size: 21pt;
color: $purple;
}
p {
display: flex;
align-items: center;
justify-content: space-evenly;
max-width: 40ch !important;
}
transition: all 0.2s ease-in-out;
}
.contact-card:hover {
margin: 0px .55em;
background-color: darken($blonde, 10%);
border-radius: 5px;
transform: scale(1.01);
}
}
@font-face {
font-family: 'Fantasque Sans Mono';
src: url('fonts/FantasqueSansMono-Regular.woff2') format('woff2');
font-weight: 400;
font-style: normal;
}

+ 1
- 0
css/katex.min.css
File diff suppressed because it is too large
View File


+ 15
- 0
diagrams/cc/delimcc.tex View File

@ -0,0 +1,15 @@
\begin{scope}[node distance=0.75cm]
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {shift};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {foo};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {bar};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {reset};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -3) {baz};
\draw [red, very thick, dashed] (-3.6, -2.625) -- (-1.89, -2.625) -- (-1.89, 0.375) -- (-3.6, 0.375) -- cycle;
\draw [arrows={Latex}-] (-4, 0.375) -- (-4, -3.375);
\end{scope}

+ 1
- 0
diagrams/eq/0cube.tex View File

@ -0,0 +1 @@
\node[draw,circle,label=right:$A$,fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i0) at (0, 0) {};

+ 4
- 0
diagrams/eq/1cube.tex View File

@ -0,0 +1,4 @@
\node[draw,circle,label=left:{$A[0/i]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i0) at (-1, 0) {};
\node[draw,circle,label=right:{$A[1/i]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i1) at (1, 0) {};
\draw (i0) -- (i1);

+ 6
- 0
diagrams/eq/2cube.tex View File

@ -0,0 +1,6 @@
\node[draw,circle,label=left:{$A[0/i, 0/j]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i0j0) at (-1, -1) {};
\node[draw,circle,label=right:{$A[1/i, 0/j]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i1j0) at (1, -1) {};
\node[draw,circle,label=left:{$A[0/i, 1/j]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i0j1) at (-1, 1) {};
\node[draw,circle,label=right:{$A[1/i, 1/j]$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i1j1) at (1, 1) {};
\draw (i0j0) -- (i1j0) -- (i1j1) -- (i0j1) -- (i0j0);

+ 5
- 0
diagrams/eq/interval.tex View File

@ -0,0 +1,5 @@
\node[draw,circle,label=below:$i_0$,fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i0) at (-1, 0) {};
\node[draw,circle,label=below:$i_1$,fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (i1) at (1, 0) {};
\draw (i0) -- (i1) node [midway, above] (seg) {seg};
% \draw[-] (i0) -- (i1);

+ 39
- 0
diagrams/gm/app_gx.tex View File

@ -0,0 +1,39 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {g};
\node (GX)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=F, xshift=0.75cm]
{@};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\draw[->] (GX) to ([shift=({-0.35cm,-0.35cm})]GX)
-- ++(0, -0.10cm)
-| (G);
\draw[->] (GX) to ([shift=({0.45cm,-0.35cm})]GX)
-| (X);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\draw[->] (Stk3.center) to (GX);
\end{scope}

+ 51
- 0
diagrams/gm/app_kgx.tex View File

@ -0,0 +1,51 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {g};
\node (KGX)
[xshift=-0.55cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=F, xshift=0.75cm]
{@};
\node (K)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=KGX, left of=KGX]
{K};
\node (GX)
[xshift=-0.45cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=KGX, right of=KGX]
{@};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\draw[->] (KGX) to (K);
\draw[->] (KGX) to (GX);
\draw[->] (GX) to ([shift=({-0.35cm,-0.35cm})]GX)
-- ++(0, -0.10cm)
-| (G);
\draw[->] (GX) to ([shift=({0.45cm,-0.35cm})]GX)
-| (X);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\draw[->] (Stk3.center) to (KGX);
\end{scope}

+ 25
- 0
diagrams/gm/entry.tex View File

@ -0,0 +1,25 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {g};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\end{scope}

+ 31
- 0
diagrams/gm/push_g.tex View File

@ -0,0 +1,31 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {g};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {};
\node (Stk4) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -3) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\draw[->] (Stk3.center) to (X |- 0, -2.25cm) -- (X);
\draw[->] (Stk4.center) to (G |- 0, -3cm) -- (G);
\end{scope}

+ 44
- 0
diagrams/gm/push_k.tex View File

@ -0,0 +1,44 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {g};
\node (GX)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=F, xshift=0.75cm]
{@};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\draw[->] (GX) to ([shift=({-0.35cm,-0.35cm})]GX)
-- ++(0, -0.10cm)
-| (G);
\draw[->] (GX) to ([shift=({0.45cm,-0.35cm})]GX)
-| (X);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {};
\node (Stk4) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -3) {};
\node (K) [right of=Stk4, xshift=1.5cm] {K};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\draw[->] (Stk3.center) to (GX);
\draw[->] (Stk4.center) to (K);
\end{scope}

+ 33
- 0
diagrams/gm/push_x.tex View File

@ -0,0 +1,33 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [inner xsep=0.01cm, inner ysep=0.03cm]
at (0, 0) {@};
\node (FG) [xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX]
{@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX]
{x};
\node (F) [xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2]
{f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2]
{g};
\draw[->] (FGX) to (X);
\draw[->] (FGX) to (FG);
\draw[->] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\node (Stk3) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -2.25) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\draw[->] (Stk3.center) to (0.5cm, -2.25cm) -- (X);
\end{scope}

+ 34
- 0
diagrams/gm/slide_3.tex View File

@ -0,0 +1,34 @@
\begin{scope}[node distance=0.75cm]
\node (KGX)
[xshift=-0.55cm, inner xsep=0.01cm, inner ysep=0.03cm]
at (0, 0) {@};
\node (K)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=KGX, left of=KGX]
{K};
\node (GX)
[xshift=-0.45cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=KGX, right of=KGX]
{@};
\node (G)
[xshift=0.45cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=GX, left of=GX]
{g};
\node (X)
[xshift=-0.45cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=GX, right of=GX]
{x};
\draw[->] (KGX) to (K);
\draw[->] (KGX) to (GX);
\draw[->] (GX) to (G);
\draw[->] (GX) to (X);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\draw[->] (Stk0.center) to (KGX);
\end{scope}

+ 25
- 0
diagrams/gm/spine+stack.tex View File

@ -0,0 +1,25 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [color=blue,inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [color=blue,xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {y};
\node (F) [color=blue,xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {x};
\draw[->] (FGX) to (X);
\draw[->,color=blue] (FGX) to (FG);
\draw[->,color=blue] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\node (Stk0) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, 0) {};
\node (Stk1) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -0.75) {};
\node (Stk2) [draw, shape=rectangle, minimum width=1.5cm, minimum height=0.75cm, anchor=center]
at (-2.75, -1.5) {};
\draw[->] (Stk0.center) to (FGX);
\draw[->] (Stk1.center) to (FG);
\draw[->] (Stk2.center) to (F);
\end{scope}

+ 14
- 0
diagrams/gm/spine.tex View File

@ -0,0 +1,14 @@
\begin{scope}[node distance=0.75cm]
\node (FGX) [color=blue,inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (FG) [color=blue,xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, left of=FGX] {@};
\node (X) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FGX, right of=FGX] {y};
\node (F) [color=blue,xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=FG, left of=FG, xshift=2] {f};
\node (G) [xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=FG, right of=FG, xshift=-2] {x};
\draw[->] (FGX) to (X);
\draw[->,color=blue] (FGX) to (FG);
\draw[->,color=blue] (FG) to (F.north east);
\draw[->] (FG) to (G.north west);
\end{scope}

+ 1
- 0
diagrams/template/step1.tex View File

@ -0,0 +1 @@
\node at (0, 0) {main};

+ 26
- 0
diagrams/template/step2.tex View File

@ -0,0 +1,26 @@
\begin{scope}[node distance=0.75cm]
\node (DoDo4) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (Do)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, left of=DoDo4]
{double};
\node (Do4)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, right of=DoDo4]
{@};
\node (Do_2)
[xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=Do4, left of=Do4, xshift=2]
{double};
\node (4)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Do4, right of=Do4, xshift=-2]
{4};
\draw[->] (DoDo4) to (Do);
\draw[->] (DoDo4) to (Do4);
\draw[->] (Do4) to (Do_2);
\draw[->] (Do4) to (4);
\end{scope}

+ 33
- 0
diagrams/template/step3.tex View File

@ -0,0 +1,33 @@
\begin{scope}[node distance=0.75cm]
\node (DoDo4) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (TimesAp)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, left of=DoDo4]
{@};
\node (Times)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=TimesAp, left of=TimesAp]
{$+$};
\node (Do4)
[xshift=-0.5cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4,
right of=DoDo4, yshift=-0.5cm]
{@};
\node (Do_2)
[xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=Do4, left of=Do4, xshift=2]
{double};
\node (4)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Do4, right of=Do4, xshift=-2]
{4};
\draw[->] (DoDo4) to (TimesAp);
\draw[->] (TimesAp) to (Times);
\draw[->] (TimesAp) |- (Do4);
\draw[->] (DoDo4) to (Do4);
\draw[->] (Do4) to (Do_2);
\draw[->] (Do4) to (4);
\end{scope}

+ 38
- 0
diagrams/template/step4.tex View File

@ -0,0 +1,38 @@
\begin{scope}[node distance=0.75cm]
\node (DoDo4) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (TimesAp)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, left of=DoDo4]
{@};
\node (Times)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=TimesAp, left of=TimesAp]
{$+$};
\node (Times44)
[xshift=-0.5cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, right of=DoDo4, yshift=-0.5cm]
{@};
\node (4)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Times44, right of=Times44, yshift=-0.75cm]
{4};
\node (Times4)
[xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=Times44, left of=Times44, xshift=2]
{@};
\node (Times2)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Times4, left of=Times4]
{$+$};
\draw[->] (DoDo4) to (TimesAp);
\draw[->] (TimesAp) to (Times);
\draw[->] (TimesAp) to (Times44);
\draw[->] (DoDo4) to (Times44);
\draw[->] (Times44) to (Times4);
\draw[->] (Times4) to (Times2);
\draw[->] (Times4) |- (4);
\draw[->] (Times44) to (4);
\end{scope}

+ 38
- 0
diagrams/template/step4red.tex View File

@ -0,0 +1,38 @@
\begin{scope}[node distance=0.75cm]
\node (DoDo4) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (TimesAp)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, left of=DoDo4]
{@};
\node (Times)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=TimesAp, left of=TimesAp]
{$+$};
\node (Times44)
[xshift=-0.5cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, right of=DoDo4, yshift=-0.5cm, color=blue]
{@};
\node (4)
[xshift=-0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Times44, right of=Times44, yshift=-0.75cm, color=blue]
{4};
\node (Times4)
[xshift=0.25cm, inner xsep=0.04cm, inner ysep=0.05cm, below of=Times44, left of=Times44, xshift=2, color=blue]
{@};
\node (Times2)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=Times4, left of=Times4, color=blue]
{$+$};
\draw[->] (DoDo4) to (TimesAp);
\draw[->] (TimesAp) to (Times);
\draw[->] (TimesAp) to (Times44);
\draw[->] (DoDo4) to (Times44);
\draw[->,color=blue,dashed] (Times44) to (Times4);
\draw[->,color=blue,dashed] (Times4) to (Times2);
\draw[->,color=blue,dashed] (Times4) |- (4);
\draw[->,color=blue,dashed] (Times44) to (4);
\end{scope}

+ 22
- 0
diagrams/template/step5.tex View File

@ -0,0 +1,22 @@
\begin{scope}[node distance=0.75cm]
\node (DoDo4) [inner xsep=0.01cm, inner ysep=0.03cm] at (0, 0) {@};
\node (TimesAp)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, left of=DoDo4]
{@};
\node (Times)
[xshift=0.25cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=TimesAp, left of=TimesAp]
{$+$};
\node (8)
[xshift=-0.5cm, inner xsep=0.01cm, inner ysep=0.03cm, below of=DoDo4, right of=DoDo4, yshift=-0.75cm]
{8};
\draw[->] (DoDo4) to (TimesAp);
\draw[->] (TimesAp) to (Times);
\draw[->] (TimesAp) |- (8);
\draw[->] (DoDo4) to (8);
\end{scope}

+ 2
- 0
hie.yaml View File

@ -0,0 +1,2 @@
cradle:
stack:

+ 140
- 0
package-lock.json View File

@ -0,0 +1,140 @@
{
"name": "blag",
"version": "1.0.0",
"lockfileVersion": 1,
"requires": true,
"dependencies": {
"anymatch": {
"version": "3.1.1",
"resolved": "https://registry.npmjs.org/anymatch/-/anymatch-3.1.1.tgz",
"integrity": "sha512-mM8522psRCqzV+6LhomX5wgp25YVibjh8Wj23I5RPkPppSVSjyKD2A2mBJmWGa+KN7f2D6LNh9jkBCeyLktzjg==",
"requires": {
"normalize-path": "^3.0.0",
"picomatch": "^2.0.4"
}
},
"binary-extensions": {
"version": "2.1.0",
"resolved": "https://registry.npmjs.org/binary-extensions/-/binary-extensions-2.1.0.tgz",
"integrity": "sha512-1Yj8h9Q+QDF5FzhMs/c9+6UntbD5MkRfRwac8DoEm9ZfUBZ7tZ55YcGVAzEe4bXsdQHEk+s9S5wsOKVdZrw0tQ=="
},
"braces": {
"version": "3.0.2",
"resolved": "https://registry.npmjs.org/braces/-/braces-3.0.2.tgz",
"integrity": "sha512-b8um+L1RzM3WDSzvhm6gIz1yfTbBt6YTlcEKAvsmqCZZFw46z626lVj9j1yEPW33H5H+lBQpZMP1k8l+78Ha0A==",
"requires": {
"fill-range": "^7.0.1"
}
},
"chokidar": {
"version": "3.4.3",
"resolved": "https://registry.npmjs.org/chokidar/-/chokidar-3.4.3.tgz",
"integrity": "sha512-DtM3g7juCXQxFVSNPNByEC2+NImtBuxQQvWlHunpJIS5Ocr0lG306cC7FCi7cEA0fzmybPUIl4txBIobk1gGOQ==",
"requires": {
"anymatch": "~3.1.1",
"braces": "~3.0.2",
"fsevents": "~2.1.2",
"glob-parent": "~5.1.0",
"is-binary-path": "~2.1.0",
"is-glob": "~4.0.1",
"normalize-path": "~3.0.0",
"readdirp": "~3.5.0"
}
},
"commander": {
"version": "2.20.3",
"resolved": "https://registry.npmjs.org/commander/-/commander-2.20.3.tgz",
"integrity": "sha512-GpVkmM8vF2vQUkj2LvZmD35JxeJOLCwJ9cUkugyk2nuhbv3+mJvpLYYt+0+USMxE+oj+ey/lJEnhZw75x/OMcQ=="
},
"fill-range": {
"version": "7.0.1",
"resolved": "https://registry.npmjs.org/fill-range/-/fill-range-7.0.1.tgz",
"integrity": "sha512-qOo9F+dMUmC2Lcb4BbVvnKJxTPjCm+RRpe4gDuGrzkL7mEVl/djYSu2OdQ2Pa302N4oqkSg9ir6jaLWJ2USVpQ==",
"requires": {
"to-regex-range": "^5.0.1"
}
},
"fsevents": {
"version": "2.1.3",
"resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.1.3.tgz",
"integrity": "sha512-Auw9a4AxqWpa9GUfj370BMPzzyncfBABW8Mab7BGWBYDj4Isgq+cDKtx0i6u9jcX9pQDnswsaaOTgTmA5pEjuQ==",
"optional": true
},
"glob-parent": {
"version": "5.1.1",
"resolved": "https://registry.npmjs.org/glob-parent/-/glob-parent-5.1.1.tgz",
"integrity": "sha512-FnI+VGOpnlGHWZxthPGR+QhR78fuiK0sNLkHQv+bL9fQi57lNNdquIbna/WrfROrolq8GK5Ek6BiMwqL/voRYQ==",
"requires": {
"is-glob": "^4.0.1"
}
},
"is-binary-path": {
"version": "2.1.0",
"resolved": "https://registry.npmjs.org/is-binary-path/-/is-binary-path-2.1.0.tgz",
"integrity": "sha512-ZMERYes6pDydyuGidse7OsHxtbI7WVeUEozgR/g7rd0xUimYNlvZRE/K2MgZTjWy725IfelLeVcEM97mmtRGXw==",
"requires": {
"binary-extensions": "^2.0.0"
}
},
"is-extglob": {
"version": "2.1.1",
"resolved": "https://registry.npmjs.org/is-extglob/-/is-extglob-2.1.1.tgz",
"integrity": "sha1-qIwCU1eR8C7TfHahueqXc8gz+MI="
},
"is-glob": {
"version": "4.0.1",
"resolved": "https://registry.npmjs.org/is-glob/-/is-glob-4.0.1.tgz",
"integrity": "sha512-5G0tKtBTFImOqDnLB2hG6Bp2qcKEFduo4tZu9MT/H6NQv/ghhy30o55ufafxJ/LdH79LLs2Kfrn85TLKyA7BUg==",
"requires": {
"is-extglob": "^2.1.1"
}
},
"is-number": {
"version": "7.0.0",
"resolved": "https://registry.npmjs.org/is-number/-/is-number-7.0.0.tgz",
"integrity": "sha512-41Cifkg6e8TylSpdtTpeLVMqvSBEVzTttHvERD741+pnZ8ANv0004MRL43QKPDlK9cGvNp6NZWZUBlbGXYxxng=="
},
"katex": {
"version": "0.11.1",
"resolved": "https://registry.npmjs.org/katex/-/katex-0.11.1.tgz",
"integrity": "sha512-5oANDICCTX0NqYIyAiFCCwjQ7ERu3DQG2JFHLbYOf+fXaMoH8eg/zOq5WSYJsKMi/QebW+Eh3gSM+oss1H/bww==",
"requires": {
"commander": "^2.19.0"
}
},
"normalize-path": {
"version": "3.0.0",
"resolved": "https://registry.npmjs.org/normalize-path/-/normalize-path-3.0.0.tgz",
"integrity": "sha512-6eZs5Ls3WtCisHWp9S2GUy8dqkpGi4BVSz3GaqiE6ezub0512ESztXUwUB6C6IKbQkY2Pnb/mD4WYojCRwcwLA=="
},
"picomatch": {
"version": "2.2.2",
"resolved": "https://registry.npmjs.org/picomatch/-/picomatch-2.2.2.tgz",
"integrity": "sha512-q0M/9eZHzmr0AulXyPwNfZjtwZ/RBZlbN3K3CErVrk50T2ASYI7Bye0EvekFY3IP1Nt2DHu0re+V2ZHIpMkuWg=="
},
"readdirp": {
"version": "3.5.0",
"resolved": "https://registry.npmjs.org/readdirp/-/readdirp-3.5.0.tgz",
"integrity": "sha512-cMhu7c/8rdhkHXWsY+osBhfSy0JikwpHK/5+imo+LpeasTF8ouErHrlYkwT0++njiyuDvc7OFY5T3ukvZ8qmFQ==",
"requires": {
"picomatch": "^2.2.1"
}
},
"sass": {
"version": "1.28.0",
"resolved": "https://registry.npmjs.org/sass/-/sass-1.28.0.tgz",
"integrity": "sha512-9FWX/0wuE1KxwfiP02chZhHaPzu6adpx9+wGch7WMOuHy5npOo0UapRI3FNSHva2CczaYJu2yNUBN8cCSqHz/A==",
"requires": {
"chokidar": ">=2.0.0 <4.0.0"
}
},
"to-regex-range": {
"version": "5.0.1",
"resolved": "https://registry.npmjs.org/to-regex-range/-/to-regex-range-5.0.1.tgz",
"integrity": "sha512-65P7iz6X5yEr1cwcgvQxbbIw7Uk3gOy5dIdtZ4rDveLqhrdJP+Li/Hx6tyK0NEb+2GCyneCMJiGqrADCSNk8sQ==",
"requires": {
"is-number": "^7.0.0"
}
}
}
}

+ 21
- 0
package.json View File

@ -0,0 +1,21 @@
{
"name": "blag",
"version": "1.0.0",
"description": "[Go here instead](https://abby.how)",
"main": "index.js",
"dependencies": {
"katex": "^0.11.1",
"sass": "^1.28.0"
},
"devDependencies": {},
"scripts": {
"up": "stack run -- build && stack run -- deploy",
"watch": "stack run -- watch"
},
"repository": {
"type": "git",
"url": "[email protected]:plt-hokusai/blag.git"
},
"author": "",
"license": "ISC"
}

+ 35
- 0
pages/contact.md View File

@ -0,0 +1,35 @@
---
title: Contact
---
Here are the easiest ways to reach me:
<style>
span#reading-length { display: none; }
</style>
<div class="contact-list">
<div class="contact-card">
<span class="username">@abby#4600</span>
My Discord friend requests are always open. Feel free to add me for questions or comments!
</div>
<div class="contact-card">
<span class="username">{abby}</span>
<span>
Message me directly on <a href="https://webchat.freenode.net/">Freenode</a> IRC, or join `##dependent` to talk about types!
</span>
</div>
</div>
If you like what I do, here are some ways you can support this blog:
<div class="contact-list">
<div class="contact-card">
<span class="username"><a href="https://ko-fi.com/pltabby">Ko-fi</a></span>
You can send me a one-time donation on Ko-Fi. Just remember not to read the name on the receipt!
(Paypal sucks)
</div>
</div>

+ 13
- 0
pages/index.html View File

@ -0,0 +1,13 @@
---
title: Home
---
<p>
You've reached Abigail's blog, a place where I exposit and reflect on programming languages and type theory.
Here's the posts I've written recently:
</p>
<h2>Posts</h2>
$partial("templates/post-list.html")$
<p>…or you can find more in the <a href="/archive.html">archives</a>.</p>

+ 14
- 0
pages/oss.md View File

@ -0,0 +1,14 @@
---
title: Open-source Licenses
---
<style>
span#reading-length { display: none; }
</style>
This blog redistributes (parts of) the following free software projects:
* **KaTeX** is a fast JavaScript library for rendering LaTeX on the client. I use it to pre-generate amazing looking mathematics at compile time. **KaTeX is licensed under the terms of the MIT license, with a copy available [here](/static/licenses/LICENSE.KaTeX)**.
* **Fantasque Sans Mono** is the programming font I've used for the past 3 years, including on this website. **Fantasque Sans Mono is distributed under the terms of the Open Font License (OFL), with a copy available [here](/static/licenses/LICENSE.FantasqueSansMono)**.

+ 308
- 0
pages/posts/2016-08-17-parsec.md View File

@ -0,0 +1,308 @@
---
title: You could have invented Parsec
date: August 17, 2016 01:29 AM
---
As most of us should know, [Parsec](https://hackage.haskell.org/package/parsec)
is a relatively fast, lightweight monadic parser combinator library.
In this post I aim to show that monadic parsing is not only useful, but a simple
concept to grok.
We shall implement a simple parsing library with instances of common typeclasses
of the domain, such as Monad, Functor and Applicative, and some example
combinators to show how powerful this abstraction really is.
---
Getting the buzzwords out of the way, being _monadic_ just means that Parsers
instances of `Monad`{.haskell}. Recall the Monad typeclass, as defined in
`Control.Monad`{.haskell},
```haskell
class Applicative m => Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
{- Some fields omitted -}
```
How can we fit a parser in the above constraints? To answer that, we must first
define what a parser _is_.
A naïve implementation of the `Parser`{.haskell} type would be a simple type
synonym.
```haskell
type Parser a = String -> (a, String)
```
This just defines that a parser is a function from a string to a result pair
with the parsed value and the resulting stream. This would mean that parsers are
just state transformers, and if we define it as a synonym for the existing mtl
`State`{.haskell} monad, we get the Monad, Functor and Applicative instances for
free! But alas, this will not do.
Apart from modeling the state transformation that a parser expresses, we need a
way to represent failure. You already know that `Maybe a`{.haskell} expresses
failure, so we could try something like this:
```haskell
type Parser a = String -> Maybe (a, String)
```
But, as you might have guessed, this is not the optimal representation either:
`Maybe`{.haskell} _does_ model failure, but in a way that is lacking. It can
only express that a computation was successful or that it failed, not why it
failed. We need a way to fail with an error message. That is, the
`Either`{.haskell} monad.
```haskell
type Parser e a = String -> Either e (a, String)
```
Notice how we have the `Maybe`{.haskell} and `Either`{.haskell} outside the
tuple, so that when an error happens we stop parsing immediately. We could
instead have them inside the tuple for better error reporting, but that's out of
scope for a simple blag post.
This is pretty close to the optimal representation, but there are still some
warts things to address: `String`{.haskell} is a bad representation for textual
data, so ideally you'd have your own `Stream`{.haskell} class that has instances
for things such as `Text`{.haskell}, `ByteString`{.haskell} and
`String`{.haskell}.
One issue, however, is more glaring: You _can't_ define typeclass instances for
type synonyms! The fix, however, is simple: make `Parser`{.haskell} a newtype.
```haskell
newtype Parser a
= Parser { parse :: String -> Either String (a, String) }
```
---
Now that that's out of the way, we can actually get around to instancing some
typeclasses.
Since the AMP landed in GHC 7.10 (base 4.8), the hierarchy of the Monad
typeclass is as follows:
```haskell
class Functor (m :: * -> *) where
class Functor m => Applicative m where
class Applicative m => Monad m where
```
That is, we need to implement Functor and Applicative before we can actually
implement Monad.
We shall also add an `Alternative`{.haskell} instance for expressing choice.
First we need some utility functions, such as `runParser`{.haskell}, that runs a
parser from a given stream.
```haskell
runParser :: Parser a -> String -> Either String a
runParser (Parser p) s = fst <$> p s
```
We could also use function for modifying error messages. For convenience, we
make this an infix operator, `<?>`{.haskell}.
```haskell
(<?>) :: Parser a -> String -> Parser a
(Parser p) <?> err = Parser go where
go s = case p s of
Left _ -> Left err
Right x -> return x
infixl 2 <?>
```
`Functor`
=======
Remember that Functor models something that can be mapped over (technically,
`fmap`-ed over).
We need to define semantics for `fmap` on Parsers. A sane implementation would
only map over the result, and keeping errors the same. This is a homomorphism,
and follows the Functor laws.
However, since we can't modify a function in place, we need to return a new
parser that applies the given function _after_ the parsing is done.
```haskell
instance Functor Parser where
fn `fmap` (Parser p) = Parser go where
go st = case p st of
Left e -> Left e
Right (res, str') -> Right (fn res, str')
```
### `Applicative`
While Functor is something that can be mapped over, Applicative defines
semantics for applying a function inside a context to something inside a
context.
The Applicative class is defined as
```haskell
class Functor m => Applicative m where
pure :: a -> m a
(<*>) :: f (a -> b) -> f a -> f b
```
Notice how the `pure`{.haskell} and the `return`{.haskell} methods are
equivalent, so we only have to implement one of them.
Let's go over this by parts.
```haskell
instance Applicative Parser where
pure x = Parser $ \str -> Right (x, str)
```
The `pure`{.haskell} function leaves the stream untouched, and sets the result
to the given value.
The `(<*>)`{.haskell} function needs to to evaluate and parse the left-hand side
to get the in-context function to apply it.
```haskell
(Parser p) <*> (Parser p') = Parser go where
go st = case p st of
Left e -> Left e
Right (fn, st') -> case p' st' of
Left e' -> Left e'
Right (v, st'') -> Right (fn v, st'')
```
### `Alternative`
Since the only superclass of Alternative is Applicative, we can instance it
without a Monad instance defined. We do, however, need an import of
`Control.Applicative`{.haskell}.
```haskell
instance Alternative Parser where
empty = Parser $ \_ -> Left "empty parser"
(Parser p) <|> (Parser p') = Parser go where
go st = case p st of
Left _ -> p' st
Right x -> Right x
```
### `Monad`
After almost a thousand words, one would be excused for forgetting we're
implementing a _monadic_ parser combinator library. That means, we need an
instance of the `Monad`{.haskell} typeclass.
Since we have an instance of Applicative, we don't need an implementation of
return: it is equivalent to `pure`, save for the class constraint.
```haskell
instance Monad Parser where
return = pure
```
The `(>>=)`{.haskell} implementation, however, needs a bit more thought. Its
type signature is
```haskell
(>>=) :: m a -> (a -> m b) -> m b
```
That means we need to extract a value from the Parser monad and apply it to the
given function, producing a new Parser.
```haskell
(Parser p) >>= f = Parser go where
go s = case p s of
Left e -> Left e
Right (x, s') -> parse (f x) s'
```
While some people think that the `fail`{.haskell} is not supposed to be in the
Monad typeclass, we do need an implementation for when pattern matching fails.
It is also convenient to use `fail`{.haskell} for the parsing action that
returns an error with a given message.
```haskell
fail m = Parser $ \_ -> Left m
```
---
We now have a `Parser`{.haskell} monad, that expresses a parsing action. But, a
parser library is no good when actual parsing is made harder than easier. To
make parsing easier, we define _combinators_, functions that modify a parser in
one way or another.
But first, we should get some parsing functions.
### any, satisfying
`any` is the parsing action that pops a character off the stream and returns
that. It does no further parsing at all.
```haskell
any :: Parser Char
any = Parser go where
go [] = Left "any: end of file"
go (x:xs) = Right (x,xs)
```
`satisfying` tests the parsed value against a function of type `Char ->
Bool`{.haskell} before deciding if it's successful or a failure.
```haskell
satisfy :: (Char -> Bool) -> Parser Char
satisfy f = d
x <- any
if f x
then return x
else fail "satisfy: does not satisfy"
```
We use the `fail`{.haskell} function defined above to represent failure.
### `oneOf`, `char`
These functions are defined in terms of `satisfying`, and parse individual
characters.
```haskell
char :: Char -> Parser Char
char c = satisfy (c ==) <?> "char: expected literal " ++ [c]
oneOf :: String -> Parser Char
oneOf s = satisfy (`elem` s) <?> "oneOf: expected one of '" ++ s ++ "'"
```
### `string`
This parser parses a sequence of characters, in order.
```haskell
string :: String -> Parser String
string [] = return []
string (x:xs) = do
char x
string xs
return $ x:xs
```
---
And that's it! In a few hundred lines, we have built a working parser combinator
library with Functor, Applicative, Alternative, and Monad instances. While it's
not as complex or featureful as Parsec in any way, it is powerful enough to
define grammars for simple languages.
[A transcription](/static/Parser.hs) ([with syntax
highlighting](/static/Parser.hs.html)) of this file is available as runnable
Haskell. The transcription also features some extra combinators for use.

+ 331
- 0
pages/posts/2016-08-23-hasochism.lhs View File

@ -0,0 +1,331 @@
---
title: Dependent types in Haskell - Sort of
date: August 23, 2016
---
**Warning**: An intermediate level of type-fu is necessary for understanding
*this post.
The glorious Glasgow Haskell Compilation system, since around version 6.10 has
had support for indexed type familes, which let us represent functional
relationships between types. Since around version 7, it has also supported
datatype-kind promotion, which lifts arbitrary data declarations to types. Since
version 8, it has supported an extension called `TypeInType`, which unifies the
kind and type level.
With this in mind, we can implement the classical dependently-typed example:
Length-indexed lists, also called `Vectors`{.haskell}.
----
> {-# LANGUAGE TypeInType #-}
`TypeInType` also implies `DataKinds`, which enables datatype promotion, and
`PolyKinds`, which enables kind polymorphism.
`TypeOperators` is needed for expressing type-level relationships infixly, and
`TypeFamilies` actually lets us define these type-level functions.
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE TypeFamilies #-}
Since these are not simple-kinded types, we'll need a way to set their kind
signatures[^kind] explicitly. We'll also need Generalized Algebraic Data Types
(or GADTs, for short) for defining these types.
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE GADTs #-}
Since GADTs which couldn't normally be defined with regular ADT syntax can't
have deriving clauses, we also need `StandaloneDeriving`.
> {-# LANGUAGE StandaloneDeriving #-}
> module Vector where
> import Data.Kind
----
Natural numbers
===============
We could use the natural numbers (and singletons) implemented in `GHC.TypeLits`,
but since those are not defined inductively, they're painful to use for our
purposes.
Recall the definition of natural numbers proposed by Giuseppe Peano in his
axioms: **Z**ero is a natural number, and the **s**uccessor of a natural number
is also a natural number.
If you noticed the bold characters at the start of the words _zero_ and
_successor_, you might have already assumed the definition of naturals to be
given by the following GADT:
< data Nat where
< Z :: Nat
< S :: Nat -> Nat
This is fine if all you need are natural numbers at the _value_ level, but since
we'll be parametrising the Vector type with these, they have to exist at the
type level. The beauty of datatype promotion is that any promoted type will
exist at both levels: A kind with constructors as its inhabitant types, and a
type with constructors as its... constructors.
Since we have TypeInType, this declaration was automatically lifted, but we'll
use explicit kind signatures for clarity.
> data Nat :: Type where
> Z :: Nat
> S :: Nat -> Nat
The `Type` kind, imported from `Data.Kind`, is a synonym for the `*` (which will
eventually replace the latter).
Vectors
=======
Vectors, in dependently-typed languages, are lists that apart from their content
encode their size along with their type.
If we assume that lists can not have negative length, and an empty vector has
length 0, this gives us a nice inductive definition using the natural number
~~type~~ kind[^kinds]
> 1. An empty vector of `a` has size `Z`{.haskell}.
> 2. Adding an element to the front of a vector of `a` and length `n` makes it
> have length `S n`{.haskell}.
We'll represent this in Haskell as a datatype with a kind signature of `Nat ->
Type -> Type` - That is, it takes a natural number (remember, these were
automatically lifted to kinds), a regular type, and produces a regular type.
Note that, `->` still means a function at the kind level.
> data Vector :: Nat -> Type -> Type where
Or, without use of `Type`,
< data Vector :: Nat -> * -> * where
We'll call the empty vector `Nil`{.haskell}. Remember, it has size
`Z`{.haskell}.
> Nil :: Vector Z a
Also note that type variables are implicit in the presence of kind signatures:
They are assigned names in order of appearance.
Consing onto a vector, represented by the infix constructor `:|`, sets its
length to the successor of the existing length, and keeps the type of elements
intact.
> (:|) :: a -> Vector x a -> Vector (S x) a
Since this constructor is infix, we also need a fixidity declaration. For
consistency with `(:)`, cons for regular lists, we'll make it right-associative
with a precedence of `5`.
> infixr 5 :|
We'll use derived `Show`{.haskell} and `Eq`{.haskell} instances for
`Vector`{.haskell}, for clarity reasons. While the derived `Eq`{.haskell} is
fine, one would prefer a nicer `Show`{.haskell} instance for a
production-quality library.
> deriving instance Show a => Show (Vector n a)