iitalics

#lang racket
(require (for-syntax syntax/parse)
         (for-meta 2 racket syntax/parse syntax/stx racket/syntax))

(begin-for-syntax
  (begin-for-syntax

    ;; attr+arity ::= id
    ;;              | [id arity]
    ;;

infinity0

(* GADT list that exposes the type of the head element *)
type _ hlist =
 | Nil: 'a hlist
 | Cons: ('a * 'b hlist) -> 'a hlist

(* let rec len = function *)
(* let rec len (type a) (l: a hlist): int = match l with *)
(* both of the above result in a "type constructor would escape its scope" error *)
(* correct version: *)
let rec len : type a. a hlist -> int = function

zmactep

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

Church Encoding

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -> (f (f x)))

lexi-lambda

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Language.HigherRank.Main
  ( Expr(..)
  , EVar(..)
  , Type(..)
  , TVar(..)
  , TEVar(..)
  , runInfer
  ) where

lexi-lambda

{-# LANGUAGE FlexibleInstances #-}

-- | An implementation of Section 3, Local Type Argument Synthesis, from the
-- paper /Local Type Inference/ by Pierce and Turner.
module Infer where

import Control.Monad (foldM, join, zipWithM)
import Data.Function (on)
import Data.List (foldl', groupBy, intercalate, intersect, nub)

Drup

type ('ty,'v) t =
  | Nil : ('v, 'v) t
  | Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t

let cons x l = Cons (x,l)

let plus1 l = Cons ((),l)

let one x = Cons (x,Nil)

tonyg

#lang racket/base
;; Simple effect system.

;; Should `with-effect` be called `with-effect-handler` (or `with-effect-handlers`)?

(provide (except-out (struct-out effect-tag) effect-tag)
         make-effect-tag
         effect-available?
         perform
         perform/abort

jwosty

open System
open System.IO

type State<'s, 'a> = State of ('s -> ('a * 's))

module State =
    let inline run state x = let (State(f)) = x in f state
    let get = State(fun s -> s, s)
    let put newState = State(fun _ -> (), newState)
    let map f s = State(fun (state: 's) ->

lexi-lambda

#lang typed/racket/base

(require (for-syntax racket/base
                     racket/sequence
                     racket/syntax
                     syntax/parse
                     syntax/stx)
         racket/match)

(begin-for-syntax

praeclarum

module Parsing

/// Remember where we are in the code.
/// This is a struct to keep memory pressure down.
/// (Significant perf improvements on iOS.)
type ParseState =
    struct
        val Code : string
        val Index : int
        new (code : string, index : int) =