kamil-adam

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

kamil-adam

(load "lazier.scm")
(load "prelude.scm")
(load "prelude-numbers.scm")

(lazy-def '(main input) '(parse-unlambda i input))

(lazy-def 'parse-unlambda
 '((lambda (x) (x x))
   (lambda (self cont input)
     ((nth (car input) dispatch-list) (self self) cont (cdr input)) )))

kamil-adam

Kodowanie Churcha

Dziś chcę opowiedzieć o kodowaniu Churcha, które jest za równo piękną konstrukcją w teorii obliczeń, jak i w praktyce.

Wymagana wiedza:

• podstawy rachunku lambda;
• podstawy Haskella (struktury danych, klasy typów; byłoby świetnie, gdybyś znał: dyrektywy RankNTypes, INLINE, SPECIALIZE, stream fusing).

Czym jest kodowanie Churcha?

kamil-adam

const I  = x => x
const K  = x => y => x
const A  = f => x => f (x)
const T  = x => f => f (x)
const W  = f => x => f (x) (x)
const C  = f => y => x => f (x) (y)
const B  = f => g => x => f (g (x))
const S  = f => g => x => f (x) (g (x))
const S_ = f => g => x => f (g (x)) (x)
const S2 = f => g => h => x => f (g (x)) (h (x))

kamil-adam

% Brainfuck interpreter written in PostScript.
%
% Written in about 2 to 3 hours around midnight. This includes the time spent
% learning PostScript, which is now the first stack-based programming language
% I've actually used. Because of this, the code is pretty ugly (even for
% PostScript), but hey, it manages to correctly interpret the "Hello world"
% example from the Wikipedia page on Brainfuck.
%
% For best results, run via `ghostscript brainfuck.ps`. Enter your brainfuck
% code at the `brainfuck> ` prompt and your program input (if necessary) at the

kamil-adam

% Representation of grammar. Nonterminals expr, term, term_tail, 
% and factor_tail are represented as non(e, _), non(t, _), non(tt, _), 
% and non(ft, _), respectively. Special nonterminal start is encoded
% as non(s, _).
% Terminals num, -, and * are represented by term(num,_), term(minus,_)
% and term(times, _). Special terminal term(eps, _) denotes the epsilon
% symbol.
% 
% Productions are represented with prod(N, [H | T]) --- that is, arguments 
% are the production index N and a list [H | T] where the head of the 

kamil-adam

package tapl;

terminals true false if then else value steporvalue Bool

syntax

t ::= true |
      false |
      if t then t else t

kamil-adam

import Text.ParserCombinators.Parsec
import System.Environment (getArgs)
import Safe

data Expr =
    Var Name            -- variable
  | App Expr Expr       -- application
  | Lambda Name Expr    -- lambda abstraction
  deriving
  (Eq,Show)

kamil-adam

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

kamil-adam

-- {-# LANGUAGE OverloadedStrings #-}

import Data.Text
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.State
import Control.Monad.Trans.Identity
import Control.Monad.Identity
import Control.Monad.Logger