pbl64k

<?hh

require_once(__DIR__ . '/soundness.hh');

breakage();

pbl64k

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

pbl64k

Fix : (Type -> Type) -> Type
Fix f = {x : Type} -> (f x -> x) -> x

fold : Functor f => {x : Type} -> (f x -> x) -> Fix f -> x
fold k t = t k

embed : Functor f => f (Fix f) -> Fix f
embed s k = k (map (fold k) s)

project : Functor f => Fix f -> f (Fix f)

pbl64k

%default total

data Mu : (Type -> Type) -> Type where
    In : f (Mu f) -> Mu f

out : Mu f -> f (Mu f)
out (In x) = x

data LstF : Type -> Type -> Type where
    LF : ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c) -> LstF a b

pbl64k

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

import Data.Maybe

data Fix f = Fix { unFix :: f (Fix f) }

data ListF a b = LF { unLF :: forall c. (Maybe (a, (c, b)) -> c) -> c }

type List a = Fix (ListF a)

pbl64k

<?hh // strict

final class Dummy<Tx> implements ConstIndexAccess<int, Tx>
{
    final public function __construct(private Tx $x) { }

    final public function at(int $ix): Tx
    {
        return $this->x;
    }

pbl64k

<?hh

    require_once(__DIR__.'/tc-bug2-minimal.hh');

    test();

pbl64k

<?hh

    require_once(__DIR__.'/tc-bug2-minimal.hh');

    test();

pbl64k

<?hh

    require_once(__DIR__.'/minimum-test.hh');

    Unsafe::test();

pbl64k

%default total

data Id : Type -> Type where
    I : a -> Id a

data Const : (a : Type) -> (b : Type) -> Type where
    K : a -> Const a b

data Sum : (a : Type -> Type) -> (b : Type -> Type) -> (c : Type) -> Type where
    SumL : a c -> Sum a b c