mb64

(* Compile with:
  $ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
Example use:
  $ ./tychk <<EOF
  > let f = (fun x -> x) : forall a. a -> a
  > in f f
  > EOF
  input : forall a. a -> a
*)

mb64

kind ty type.

type tunit  ty.
type tfun   ty -> ty -> ty.
type tall   (ty -> ty) -> ty.

kind tm type.

type unit   tm.
type app    tm -> tm -> tm.

pdarragh

Approachable PL Papers for Undergrads

On September 28, 2021, I asked on Twitter:

PL Twitter:

you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.

what paper do you recommend?

MrSmith33

Source code: https://github.com/MrSmith33/voxelman/blob/master/source/voxelman/gui

Core widget components (https://github.com/MrSmith33/voxelman/blob/master/source/voxelman/gui/components.d):

• WidgetTransform - main component of any widget. Stores parent reference, relative position, absolute position, size, min size, measured size, and extra flags
• WidgetStyle - color and border color
• WidgetName - string of widget name
• WidgetType - string of widget type (for debugging)
• WidgetContainer - children widgets
• WidgetIsFocusable - if set becomes focusedWidget on pointer press. focusedWidget will receive key and char events.
• WidgetEvents - stores handlers for any event for the widget. Typical events:

robrix

type Name = String

-- first-order syntax
data Tm
  = Var Name
  | Abs Name Tm
  | App Tm Tm
  deriving (Eq, Ord, Show)

type Env = [(Name, Val)]

andrejbauer

open import Data.Bool
open import Data.Empty
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality

module Corey where

  -- streams of bits
  record Stream : Set where

AndrasKovacs

{-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

module UnivPoly where

import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace

hwayne

class Bank:
    def __init__(self, balance):
        assert balance > 0
        self.balance = balance
    
    def deposit(self, val):
        self.balance += val
    
    def withdraw(self, val):
        if val <= self.balance:

keleshev

(* https://keleshev.com/advanced-error-handling-in-ocaml *)

let failwithf f = Printf.ksprintf failwith f

(*

  t -> bool | int

  e -> true | false
     | 0 | 1 | 2 | …

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module ObfuscatedSKI where

import Unsafe.Coerce (unsafeCoerce)

--------------------------------------------------------------------------------
-- A Lambda to SKI Combinator Compiler, written entirely using SKI Combinators
--