edmundsmith

Method for Emulating Higher-Kinded Types in Rust

Intro

I've been fiddling about with an idea lately, looking at how higher-kinded types can be represented in such a way that we can reason with them in Rust here and now, without having to wait a couple years for what would be a significant change to the language and compiler.

There have been multiple discussions on introducing higher-ranked polymorphism into Rust, using Haskell-style Higher-Kinded Types (HKTs) or Scala-looking Generalised Associated Types (GATs). The benefit of higher-ranked polymorphism is to allow higher-level, richer abstractions and pattern expression than just the rank-1 polymorphism we have today.

As an example, currently we can express this type:

AndrasKovacs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val

romainl

Don't use Vim

Don't do the crime, if you can't do the time.

-- Anthony Vincenzo "Tony" Baretta

Vim is an amazing text editor. I love it. Really, I wouldn't [organize][organize] a Vim advent calendar if I didn't. But, as amazing as it is, Vim is not for everyone. It can't solve all your problems, or be a TUI version of your favorite IDE, or make you a better programmer, or land you that dream job in the Bay Area. But Vim can help you be more mindful, focused, and efficient, as long as you approach it with the right mindset.

Don't get me wrong, I certainly welcome you to try Vim, but I'm not a proselyte. I don't thrive on newbies. I just want you to use the right tool for the job and not waste your—and anyone's—time on a fruitless quest.

notfoundry

const static struct _0 {} _0;
const static struct _1 {} _1;


#define G7_SPLICE(expr) __typeof__(expr)

#define G7_STRUCT(...) (struct { __VA_ARGS__ } ){}


#define G7_NAND(a, b)                                  \

lukaszlew

-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}

-- File mnemonics:
--   env = typing environment
--   vid = variable identifier in Bind or Var
--   br = binder variant (Lambda or Pi)
--   xyzTyp = type of xyz
--   body = body of Lambda or Pi abstraction

hirrolot

data Fmt = FArg Fmt | FChar Char Fmt | FEnd

toFmt : (fmt : List Char) -> Fmt
toFmt ('*' :: xs) = FArg (toFmt xs)
toFmt (  x :: xs) = FChar x (toFmt xs)
toFmt [] = FEnd

PrintfType : (fmt : Fmt) -> Type
PrintfType (FArg fmt) = ({ty : Type} -> Show ty => (obj : ty) -> PrintfType fmt)
PrintfType (FChar _ fmt) = PrintfType fmt

hirrolot

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

hirrolot

trait Interp {
    type Repr<T>;

    fn lit(i: i32) -> Self::Repr<i32>;
    fn add(a: Self::Repr<i32>, b: Self::Repr<i32>) -> Self::Repr<i32>;
}

struct Eval;

impl Interp for Eval {

hirrolot

let rec eval = function
  | `Appl (m, n) -> (
      let n' = eval n in
      match eval m with `Lam f -> eval (f n') | m' -> `Appl (m', n'))
  | (`Lam _ | `Var _) as t -> t

let sprintf = Printf.sprintf

(* Print a given term using De Bruijn levels. *)
let rec pp lvl = function