praeclarum

module k


(*

type TypeIdent = string

type TypeExpr = name:string? (string | TypeIdent | Or TypeExpr TypeExpr | And TypeExpr)

type TypeDecl = Type string TypeExpr

praeclarum

module AlgorithmW

// HINDLEY-MILNER TYPE INFERENCE
// Based on http://catamorph.de/documents/AlgorithmW.pdf
// (Now at http://web.archive.org/web/20170704013532/http://catamorph.de/documents/AlgorithmW.pdf)

type Lit =
    | LInt of int
    | LBool of bool

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) =

lexi-lambda

#lang typed/racket/base

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

(begin-for-syntax

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) ->

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

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)

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)

lexi-lambda

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

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

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)))