\gdef\jdg#1{\:\mathrm{#1}}
\gdef\decode#1{\mathord{\uparrow}#1}
\gdef\code#1{\mathord{\downarrow}#1}
\gdef\jty{\:\mathrm{ty}}
\gdef\jprop{\:\mathrm{prop}}
\gdef\jtrue{\:\mathrm{true}}
\gdef\yields{\vdash}
\gdef\ms#1{\mathsf{#1}}
\gdef\mc#1{\mathcal{#1}}
\gdef\Open#1{{\Large \circ}{#1}}
\gdef\Close#1{{\Large \bullet}{#1}}
\gdef\OpenEta{\eta^{\circ}}
\gdef\CloseEta{\eta^{\bullet}}
\gdef\isStatic#1{\mathrm{isStatic}(#1)}
\gdef\isDynamic#1{\mathrm{isDynamic}(#1)}
\gdef\ite#1#2#3{\mathbf{if}\:\:#1\:\:\mathbf{then}\:\:#2\:\:\mathbf{else}\:\:#3}
\gdef\StOpn{{\Large \circ}_{\mathrm{st}}}
\gdef\Opn{{\Large \circ}}
\gdef\op{^\mathrm{op}}
\gdef\CC{\mathbb{C}}
Future work
-
Write a compiler for hippogriff
-
Use relative induction principles to show that we have static normalization
-
Investigate denotational semantics for the recursion
-
Pattern unification
-
Extension types
-
Dynamic modules
-
Compile-time inductive types (zig’s comptime)
-
Compile-time propositions with a datalog-based solver (typeclasses)