AlgorithmWTest.php

<?php

declare(strict_types=1);

namespace AlgorithmW;

/*
data Exp
    = EVar String
    | ELit Lit
    | EApp Exp Exp
    | EAbs String Exp
    | ELet String Exp Exp
    deriving (Eq,Ord)

data Lit
    = LInt Integer
    | LBool Bool deriving (Eq,Ord)

data Type
    = TVar String
    | TInt
    | TBool
    | TFun Type Type
    deriving (Eq,Ord)

data Scheme = Scheme [ String ] Type

*/

use PHPUnit\Runner\Exception;
use Widmogrod\Monad\Maybe\Just;
use Widmogrod\Monad\Maybe\Maybe;
use Widmogrod\Monad\Maybe\Nothing;
use Widmogrod\Primitive\Listt;
use Widmogrod\Useful\PatternMatcher;
use function Widmogrod\Functional\curryN;
use function Widmogrod\Functional\foldr;
use function Widmogrod\Functional\fromNil;
use function Widmogrod\Functional\map;
use function Widmogrod\Functional\zip;
use function Widmogrod\Useful\match;
use const Widmogrod\Functional\identity;
use const Widmogrod\Useful\any;

interface Exp extends PatternMatcher
{
}

class EVar implements Exp
{
    private $string;

    public function __construct($string)
    {
        $this->string = $string;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->string);
    }
}

class ELit implements Exp
{
    private $lit;

    public function __construct(Lit $lit)
    {
        $this->lit = $lit;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->lit);
    }
}

class EApp implements Exp
{
    private $exp1;
    private $exp2;

    public function __construct(Exp $exp1, Exp $exp2)
    {
        $this->exp1 = $exp1;
        $this->exp2 = $exp2;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->exp1, $this->exp2);
    }
}

class EAbs implements Exp
{
    private $string;
    private $exp;

    public function __construct($string, Exp $exp)
    {
        $this->string = $string;
        $this->exp = $exp;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->string, $this->exp);
    }
}

class ELet implements Exp
{
    private $string;
    private $exp1;
    private $exp2;

    public function __construct($string, Exp $exp1, Exp $exp2)
    {
        $this->string = $string;
        $this->exp1 = $exp1;
        $this->exp2 = $exp2;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->string, $this->exp1, $this->exp2);
    }
}

interface Lit extends PatternMatcher
{
}

class LInt implements Lit
{
    private $int;

    public function __construct(int $int)
    {
        $this->int = $int;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->int);
    }
}

class LBool implements Lit
{
    private $bool;

    public function __construct(bool $bool)
    {
        $this->bool = $bool;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->bool);
    }
}

interface Type extends PatternMatcher
{
}

class TVar implements Type
{
    private $string;

    public function __construct(string $string)
    {
        $this->string = $string;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->string);
    }
}

class TInt implements Type
{
    public function patternMatched(callable $fn)
    {
        return $fn();
    }
}

class TBool implements Type
{
    public function patternMatched(callable $fn)
    {
        return $fn();
    }
}

class TFun implements Type
{
    private $type1;
    private $type2;

    public function __construct(Type $type1, Type $type2)
    {
        $this->type1 = $type1;
        $this->type2 = $type2;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->type1, $this->type2);
    }
}

// data Scheme = Scheme [ String ] Type
class Scheme implements PatternMatcher
{
    /**
     * @var array
     */
    private $strings;
    private $type;

    public function __construct(Listt $strings, Type $type)
    {
        $this->strings = $strings;
        $this->type = $type;
    }

    public function patternMatched(callable $fn)
    {
        return $fn($this->strings, $this->type);
    }
}

function union(Set $a, Set $b): Set
{
    return Set::union($a, $b);
}

function difference(Set $a, Set $b): Set
{
    return Set::difference($a, $b);
}


function lookup(Map $map, string $key): Maybe
{
    return $map::lookup($key, $map);
}

// type Subst = Map.Map String Type
class Subst extends Map
{
}

const nullSubst = 'AlgorithmW\nullSubst';

// nullSubst :: Subst
// nullSubst = Map.empty
function nullSubst(): Subst
{
    return Subst::mempty();
}

const composeSubst = 'AlgorithmW\composeSubst';

// composeSubst :: Subst → Subst → Subst
// composeSubst s1 s2 = (Map.map (apply s1) s2) ‘Map.union‘ s1
function composeSubst(Subst $s1, Subst $s2): Subst
{
    return Subst::union(
        Subst::map(apply($s1), $s2),
        $s1
    );
}

// newtype TypeEnv = TypeEnv (Map.Map String Scheme)
class TypeEnv implements PatternMatcher
{
    private $env;

    public function __construct(Map $env)
    {
        $this->env = $env;
    }

    /**
     * @inheritdoc
     */
    public function patternMatched(callable $fn)
    {
        return $fn($this->env);
    }
}

// remove :: TypeEnv → String → TypeEnv
// remove (TypeEnv env) var = TypeEnv (Map.delete var env)

function remove(TypeEnv $env, $var): TypeEnv
{
    return new TypeEnv(Map::delete($var, $env));
}

// generalize :: TypeEnv → Type → Scheme
// generalize env t = Scheme vars t
//      where vars = Set.toList ((ftv t) \ (ftv env))
function generalize(TypeEnv $env, Type $t): Scheme
{
    return new Scheme(
        Set::toList(difference(ftv($t), ftv($env))),
        $t
    );
}

const ftv = 'AlgorithmW\ftv';

/**
 * ftv :: a → Set.Set String
 *
 * @param  Type|Listt|Scheme|TypeEnv                $t
 * @return Set
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function ftv($t): Set
{
    return match([
        // instance Types Type where
        TVar::class => function ($n): Set {
            return Set::withValue($n);
        },
        TBool::class => function (): Set {
            return Set::mempty();
        },
        TInt::class => function (): Set {
            return Set::mempty();
        },
        TFun::class => function (Type $a, Type $b): Set {
            return union(ftv($a), ftv($b));
        },
        // instance Types Scheme where
        Scheme::class => function (Listt $vars, Type $t): Set {
            // ftv (Scheme vars t) = (ftv t) \ (Set.fromList vars)
            return difference(ftv($t), Set::fromList($vars));
        },
        // instance Types a ⇒ Types [a] where
        Listt::class => function (Listt $l): Set {
            // ftv l = foldr Set.union ∅ (map ftv l)
            return foldr(Set::union, Set::mempty(), map(ftv, $l));
        },
        // instance Types TypeEnv where
        TypeEnv::class => function (Map $env): Set {
            // ftv (TypeEnv env) = ftv (Map.elems env)
            return ftv(Map::elems($env));
        },
    ], $t);
}

/**
 * // apply :: Subst → a → a
 *
 * @param Subst $s
 * @param Type|Scheme|Listt|TypeEnv ?$a
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function apply(Subst $s, $a = null)
{
    return curryN(2, function (Subst $s, $a) {
        return match([
            // instance Types Type where
            TVar::class => function ($n) use ($s, $a) {
                return match([
                    Just::class => identity,        // Justt → t
                    Nothing::class => function () use ($a) {
                        return $a;
                    },   // Nothing → TVar n
                ], lookup($s, $n));
            },
            TFun::class => function (Type $t1, Type $t2) use ($s) {
                return new TFun(apply($s, $t1), apply($s, $t2));
            },
            TBool::class => function () use ($a) {
                return $a;
            },
            TInt::class => function () use ($a) {
                return $a;
            },
            // instance Types Scheme where
            Scheme::class => function (Listt $vars, Type $t) use ($s) {
                // apply s (Scheme vars t) = Scheme vars (apply (foldr Map.delete s vars) t)
                return new Scheme(
                    $vars,
                    apply(foldr(function (string $var, Subst $sub) {
                        return Subst::delete($var, $sub);
                    }, $s, $vars), $t)
                );
            },
            // instance Types a ⇒ Types [a] where
            Listt::class => function (Listt $l) use ($s) {
                // apply s = map (apply s)
                return map(apply($s), $l);
            },
            // instance Types TypeEnv where
            TypeEnv::class => function (Map $env) use ($s) {
                // apply s (TypeEnv env) = TypeEnv (Map.map (apply s) env)
                return new TypeEnv(Map::map(apply($s), $env));
            },
        ], $a);
    })(...func_get_args());
}

$increment = 0;

function newVar($name)
{
    global $increment;

    return new TVar(sprintf('%s%d', $name, ++$increment));
}

// instantiate :: Scheme → TI Type
function instantiate(Scheme $s)
{
    return match([
        Scheme::class => function (Listt $vars, Type $t) {
            $nvars = map(function () {
                return newVar('a');
            }, $vars);

            $s = Subst::fromList(zip($vars, $nvars));

            return apply($s, $t);
        },
    ], $s);
}

/**
 * @param  Lit                                      $li
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function tiLit(Lit $li)
{
    return match([
        LInt::class => function () {
            return [nullSubst(), new TInt()];
        },
        LBool::class => function () {
            return [nullSubst(), new TBool()];
        },
    ], $li);
}

/**
 * @param  Type                                     $a
 * @param  Type                                     $b
 * @return Subst
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function mgu(Type $a, Type $b): Subst
{
    return match([
        [[TFun::class, TFun::class], function (Type $l1, Type $r1, Type $l2, Type $r2) {
            $s1 = mgu($l1, $l2);
            $s2 = mgu(apply($s1, $r1), apply($s1, $r2));

            return composeSubst($s1, $s2);
        }],
        [[TInt::class, TInt::class], function () {
            return Subst::mempty();
        }],
        [[TBool::class, TBool::class], function () {
            return Subst::mempty();
        }],
        [[TVar::class, any], function ($n, Type $t) {
            return varBind($n, $t);
        }],
        [[any, TVar::class], function (Type $t, $n) {
            return varBind($n, $t);
        }],
        [[any, any], function (Type $a, Type $b) {
            $message = sprintf('types do not unify: %s != %s', showType($a), showType($b));
            throw new Exception($message);
        }],
    ], [$a, $b]);
}

/**
 * @param $u
 * @param  Type                                     $t
 * @return Subst
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function varBind($u, Type $t): Subst
{
    return match([
        TVar::class => function ($n) use ($u, $t) {
            if ($n === $u) {
                return nullSubst();
            }

            return Subst::singleton($u, $t);
        },
        any => function (Type $t) use ($u) {
            if (Set::member($u, ftv($t))) {
                $message = 'occurs check fails: %s vs %s ftv(%s)';
                $message = sprintf($message, $u, dump($t), dump(ftv($t)));
                throw new Exception($message);
            }

            return Subst::singleton($u, $t);
        },
    ], $t);
}

/**
 * ti :: TypeEnv → Exp → TI (Subst , Type )
 *
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function ti(TypeEnv $env, Exp $e)
{
    return match([
        TypeEnv::class => function (Map $envMap) use ($env, $e) {
            return match([
                EVar::class => function ($n) use ($envMap) {
                    return match([
                        Nothing::class => function () use ($n) {
                            throw new Exception('unbound variable ' . $n);
                        },
                        Just::class => function ($sigma) {
                            return [nullSubst(), instantiate($sigma)];
                        },
                    ], Map::lookup($n, $envMap));
                },
                ELit::class => function (Lit $l) {
                    return tiLit($l);
                },
                EAbs::class => function ($n, Exp $e) use ($env, $envMap) {
                    $tv = newVar('a');
                    $sk = new Scheme(fromNil(), $tv);
                    $env = new TypeEnv(Map::insert($n, $sk, $envMap));

                    [$s1, $t1] = ti($env, $e);

                    return [$s1, new TFun(apply($s1, $tv), $t1)];
                },
                EApp::class => function (Exp $e1, Exp $e2) use ($env, $envMap) {
                    $tv = newVar('a');
                    [$s1, $t1] = ti($env, $e1);
                    [$s2, $t2] = ti(apply($s1, $env), $e2);
                    $s3 = mgu(apply($s2, $t1), new TFun($t2, $tv));

                    return [composeSubst($s3, composeSubst($s2, $s1)), apply($s3, $tv)];
                },
                ELet::class => function ($n, Exp $e1, Exp $e2) use ($env, $envMap) {
                    [$s1, $t1] = ti($env, $e1);
                    $sk = generalize(apply($s1, $env), $t1);
                    $env = new TypeEnv(Map::insert($n, $sk, $envMap));
                    [$s2, $t2] = ti(apply($s1, $env), $e2);

                    return [composeSubst($s1, $s2), $t2];
                },
            ], $e);
        },
    ], $env);
}

const dump = 'AlgorithmW\dump';

function dump($a)
{
    return match([
        Subst::class => function (Subst $s) {
            return iterator_to_array(Subst::elems($s));
        },
        TInt::class => function () use ($a) {
            return showType($a);
        },
        TBool::class => function () use ($a) {
            return showType($a);
        },
        TFun::class => function () use ($a) {
            return showType($a);
        },
        TVar::class => function () use ($a) {
            return showType($a);
        },
        TypeEnv::class => function (Map $env) {
            return sprintf('TypeEnv(%s)', dump($env));
        },

        Scheme::class => function (Listt $vars, Type $t) {
            return sprintf(
                'Scheme([%s], %s)',
                implode(',', iterator_to_array($vars)),
                dump($t)
            );
        },
        Listt::class => function (Listt $l) {
            return sprintf('[%s]', implode(', ', iterator_to_array($l)));
        },
        Subst::class => function (Map $map) {
            return dump(map(function (array $tuple) {
                [$a, $b] = $tuple;

                return sprintf('(%s, %s)', $a, $b);
            }, zip(
                Subst::keys($map),
                Subst::elems(Map::map(dump, $map))
            )));
        },
        Map::class => function (Map $map) {
            return dump(map(function (array $tuple) {
                [$a, $b] = $tuple;

                return sprintf('(%s, %s)', $a, $b);
            }, zip(
                Map::keys($map),
                Map::elems(Map::map(dump, $map))
            )));
        },
        Set::class => function (Set $s) {
            return sprintf('{%s}', implode(',', iterator_to_array(Set::toList($s))));
        },
    ], $a);
}

/**
 * // typeInference :: Map.Map String Scheme → Exp → TI Type
 * @param  \AlgorithmW\Map                          $env
 * @param  Exp                                      $e
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function typeInference(Map $env, Exp $e)
{
    [$s, $t] = ti(new TypeEnv($env), $e);

    return apply($s, $t);
}

/**
 * @param  Type                                     $t
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function showType(Type $t)
{
    return match([
        TInt::class => function () {
            return 'Int';
        },
        TBool::class => function () {
            return 'Bool';
        },
        TVar::class => function ($n) {
            return $n;
        },
        TFun::class => function (Type $t1, Type $t2) {
            return sprintf('(%s -> %s)', showType($t1), showType($t2));
        }
    ], $t);
}

/**
 * @param  Type                                     $t
 * @return mixed
 * @throws \Widmogrod\Useful\PatternNotMatchedError
 */
function showImpl(Exp $e)
{
    return match([
        ELit::class => match([
            LInt::class => identity,
            LBool::class => function ($val) {
                return $val ? 'true' : 'false';
            },
        ]),
        EVar::class => function ($n) {
            return $n;
        },
        ELet::class => function ($n, Exp $e1, Exp $e2) {
            return sprintf('let %s = %s in %s', $n, showImpl($e1), showImpl($e2));
        },
        EApp::class => function (Exp $e1, Exp $e2) {
            return sprintf('%s %s', showImpl($e1), showImpl($e2));
        },
        EAbs::class => function ($arg, Exp $e) {
            return sprintf('(%s -> %s)', $arg, showImpl($e));
        }
    ], $e);
}

class AlgorithmWTest extends \PHPUnit\Framework\TestCase
{
    /**
     * @dataProvider provideAlgorithmWs
     */
    public function test(Exp $expression, $expected, $error = null)
    {
        // TODO fix this hack
        global $increment;
        $increment = 0;

        if ($error) {
            $this->expectExceptionMessage($error);
        }

        // echo showImpl($expression), "\n";
        $this->assertInstanceOf(Exp::class, $expression);
        $result = typeInference(Map::mempty(), $expression);
        $this->assertEquals($expected, showType($result));
    }

    public function provideAlgorithmWs()
    {
        return [
            '2' => [
                'expression' => new ELit(new LInt(2)),
                'expected' => 'Int',
            ],
            '(x -> x)' => [
                'expression' => new EAbs(
                    'x',
                    new EVar('x')
                ),
                'expected' => '(a1 -> a1)',
            ],
            'let id = (x -> let y = (z -> let v = z in v) in y) in id id' => [
                'expression' => new ELet(
                    'id',
                    new EAbs(
                        'x',
                        new ELet(
                            'y',
                            new EAbs(
                                'z',
                                new ELet(
                                    'v',
                                    new EVar('z'),
                                    new EVar('v')
                                )
                            ),
                            new EVar('y')
                        )
                    ),
                    new EApp(
                        new EVar('id'),
                        new EVar('id')
                    )
                ),
                'expected' => '(a8 -> a8)',
            ],
            'let id = (x -> true) in id' => [
                'expression' => new ELet(
                    'id',
                    new EAbs("x", new ELit(new LBool(true))),
                    new EVar("id")
                ),
                'expected' => '(a2 -> Bool)',
            ],
            'let id = 2 in id' => [
                'expression' => new ELet(
                    'id',
                    new ELit(new LInt(2)),
                    new EVar("id")
                ),
                'expected' => 'Int',
            ],
            // e0 = ELet "id" (EAbs "x" (EVar "x")) (EVar "id")
            'let id = (x -> x) in id)' => [
                'expression' => new ELet(
                    'id',
                    new EAbs("x", new EVar("x")),
                    new EVar("id")
                ),
                'expected' => '(a2 -> a2)',
            ],
            // e1 = ELet "id" (EAbs "x" (EVar "x")) (EApp (EVar "id") (EVar "id"))
            'let id = (x -> x) in id id' => [
                'expression' => new ELet(
                    'id',
                    new EAbs(
                        'x',
                        new EVar('x')
                    ),
                    new EApp(
                        new EVar('id'),
                        new EVar('id')
                    )
                ),
                'expected' => '(a5 -> a5)',
            ],
            // e2 = ELet "id" (EAbs "x" (ELet "y" (EVar "x") (EVar "y"))) (EApp (EVar "id") (EVar "id"))
            'let id = (x -> let y = x in y) in id id ' => [
                'expression' => new ELet(
                    'id',
                    new EAbs(
                        'x',
                        new ELet(
                            'y',
                            new EVar('x'),
                            new EVar('y')
                        )
                    ),
                    new EApp(
                        new EVar('id'),
                        new EVar('id')
                    )
                ),
                'expected' => '(a5 -> a5)',
            ],
            // e3 = ELet "id" (EAbs "x" (ELet "y" (EVar "x") (EVar "y"))) (EApp (EApp (EVar "id") (EVar "id")) (ELit (LInt 2)))
            'let id = (x -> let y = x in y) in id id 2' => [
                'expression' => new ELet(
                    'id',
                    new EAbs(
                        'x',
                        new ELet(
                            'y',
                            new EVar('x'),
                            new EVar('y')
                        )
                    ),
                    new EApp(
                        new EApp(
                            new EVar('id'),
                            new EVar('id')
                        ),
                        new ELit(new LInt(2))
                    )
                ),
                'expected' => 'Int',
            ],
            // e4 = ELet "id" (EAbs "x" (EApp (EVar "x") (EVar "x"))) (EVar "id")
            'let id = (x -> x x) in id' => [
                'expression' => new ELet(
                    'id',
                    new EAbs(
                        'x',
                        new EApp(
                            new EVar('x'),
                            new EVar('x')
                        )
                    ),
                    new EVar('id')
                ),
                'expected' => null,
                'error' => 'occurs check fails: a1 vs (a1 -> a2)'
            ],
            // e5 = EAbs "m" (ELet "y" (EVar "m")
            //       (ELet "x" (EApp (EVar "y") (ELit (LBool True)))
            //          (EVar "x")))
            '(m -> let y = m in let x = y true in x)' => [
                'expression' => new EAbs(
                    'm',
                    new ELet(
                        'y',
                        new EVar('m'),
                        new ELet(
                            'x',
                            new EApp(
                                new EVar('y'),
                                new ELit(new LBool(true))
                            ),
                            new EVar('x')
                        )
                    )
                ),
                'expected' => '((Bool -> a2) -> a2)',
            ],
            // e6 = EApp (ELit (LInt 2)) (ELit (LInt 2))
            '2 2' => [
                'expression' => new EApp(
                    new ELit(new LInt(2)),
                    new ELit(new LInt(2))
                ),
                'expected' => null,
                'error' => 'types do not unify: Int != (Int -> a1)',
            ],
            // e7 = ELet "id" (EAbs "x" (EVar "y")) (EVar "id")
            'let id = (x -> y) in id' => [
                'expression' => new ELet(
                    'id',
                    new EAbs("x", new EVar("y")),
                    new EVar("id")
                ),
                'expected' => null,
                'error' => 'unbound variable y',
            ],
        ];
    }
}