use function Widmogrod\Monad\Maybe\nothing;
use function Widmogrod\Useful\match;
use const Widmogrod\Functional\identity;
+use const Widmogrod\Useful\any;
interface Exp extends PatternMatcher
{
{
const union = 'example\\Set::union';
- private static $data;
+ private $data;
private function __construct(\ArrayObject $data)
{
- self::$data = $data;
+ $this->data = $data;
}
/**
public static function toList(Set $set): Listt
{
- return fromIterable(array_keys($set::$data->getArrayCopy()));
+ return fromIterable(array_keys($set->data->getArrayCopy()));
}
public static function withValue($n): Set
public static function insert($value, Set $set): Set
{
- $new = clone $set::$data;
+ $new = clone $set->data;
$new[$value] = true;
+
return new static($new);
}
public static function difference(Set $a, Set $b): Set
{
- $diffA = reduce(function (Set $acc, $value) use ($b) {
+ return reduce(function (Set $acc, $value) use ($b) {
return static::member($value, $b)
? $acc
: static::insert($value, $acc);
}, static::mempty(), static::toList($a));
- $diffB = reduce(function (Set $acc, $value) use ($a) {
- return static::member($value, $a)
- ? $acc
- : static::insert($value, $acc);
- }, static::mempty(), static::toList($b));
-
- return static::union($diffA, $diffB);
}
- private static function member($value, Set $set): bool
+ public static function member($value, Set $set): bool
{
- return isset($set::$data[$value]);
+ return isset($set->data[$value]);
}
}
class Map
{
- const delete = 'Map::delete';
-
- protected static $data;
+ private $data;
private function __construct(\ArrayObject $data)
{
- self::$data = $data;
+ $this->data = $data;
}
public static function mempty()
public static function elems(Map $map): Listt
{
- return fromIterable(array_keys($map::$data->getArrayCopy()));
+ return fromIterable(array_values($map->data->getArrayCopy()));
+ }
+
+
+ public static function keys(Map $map): Listt
+ {
+ return fromIterable(array_keys($map->data->getArrayCopy()));
}
public static function union(Map $a, Map $b): Map
{
return reduce(function (Map $acc, $key) use ($b) {
- return static::insert($key, $b::$data[$key], $acc);
- }, $a, static::elems($b));
+ return static::insert($key, $b->data[$key], $acc);
+ }, $a, static::keys($b));
}
public static function map(callable $fn, Map $map): Map
{
return reduce(function (Map $acc, $key) use ($fn, $map) {
- return static::insert($key, $fn($map::$data[$key]), $acc);
- }, static::mempty(), static::elems($map));
+ return static::insert($key, $fn($map->data[$key]), $acc);
+ }, static::mempty(), static::keys($map));
}
public static function lookup($key, Map $map): Maybe
{
- return isset($map::$data[$key])
- ? just($map::$data[$key])
+ return isset($map->data[$key])
+ ? just($map->data[$key])
: nothing();
}
public static function delete($key, Map $map): Map
{
- $new = clone $map::$data;
- unset($new[$key]);
- return new static($new);
+ if (isset($map->data[$key])) {
+ $new = clone $map->data;
+ unset($new[$key]);
+
+ return new static($new);
+ }
+
+ return $map;
}
public static function insert($key, $value, Map $map): Map
{
- $new = clone $map::$data;
+ $new = clone $map->data;
$new[$key] = $value;
+
return new static($new);
}
{
return reduce(function (Map $acc, $tuple) {
[$key, $value] = $tuple;
+
return static::insert($key, $value, $acc);
}, static::mempty(), $list);
}
+
+ public static function singleton($u, $t)
+ {
+ return static::insert($u, $t, static::mempty());
+ }
}
function lookup(Map $map, string $key): Maybe
}
// type Subst = Map.Map String Type
-class Subst extends Map implements PatternMatcher
+class Subst extends Map
{
- /**
- * should be used with conjuction
- * @param callable $fn
- * @return mixed
- */
- public function patternMatched(callable $fn)
- {
- throw new Exception('not implemented');
- // TODO: Implement patternMatched() method.
- }
}
const nullSubst = 'example\nullSubst';
/**
* ftv :: a → Set.Set String
*
- * @param Type|Listt|Scheme|TypeEnv $t
+ * @param Type|Listt|Scheme|TypeEnv $t
* @return Set
* @throws \Widmogrod\Useful\PatternNotMatchedError
*/
// apply s (Scheme vars t) = Scheme vars (apply (foldr Map.delete s vars) t)
return new Scheme(
$vars,
- apply(foldr(Map::delete, $s, $vars), $t)
+ apply(foldr(function (string $var, Subst $sub) {
+ return Subst::delete($var, $sub);
+ }, $s, $vars), $t)
);
},
// instance Types a ⇒ Types [a] where
})(...func_get_args());
}
-// data TIEnv = TIEnv { }
-// data TIState = TIState{tiSupply :: Int }
-// type TI a = ErrorT String (ReaderT TIEnv (StateT TIState IO)) a
-//class TI
-
$increment = 0;
function newVar($name)
{
global $increment;
+
return new TVar(sprintf('%s%d', $name, ++$increment));
}
// instantiate :: Scheme → TI Type
function instantiate(Scheme $s)
{
- // instantiate (Scheme vars t)
- // = do nvars ← mapM (λ → newTyVar "a") vars
- // let s = Map.fromList (zip vars nvars)
- // return $ apply s t
return match([
Scheme::class => function (Listt $vars, Type $t) {
$nvars = map(function () {
}, $vars);
$s = Subst::fromList(zip($vars, $nvars));
+
return apply($s, $t);
},
], $s);
}
-/*
-tiLit :: Lit → TI (Subst , Type )
-tiLit (LInt ) = return (nullSubst, TInt)
-tiLit (LBool ) = return (nullSubst, TBool)
-*/
/**
- * @param Lit $li
+ * @param Lit $li
* @return mixed
* @throws \Widmogrod\Useful\PatternNotMatchedError
*/
}
/**
+ * @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
return match([
EVar::class => function ($n) use ($envMap) {
return match([
- Nothing::class => function () {
- throw new Exception('not implemented');
+ Nothing::class => function () use ($n) {
+ throw new Exception('unbound variable ' . $n);
},
Just::class => function ($sigma) {
return [nullSubst(), instantiate($sigma)];
return tiLit($l);
},
EAbs::class => function ($n, Exp $e) use ($env, $envMap) {
-// throw new Exception('not implemented');
$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($tv, $t1)];
+ return [$s1, new TFun(apply($s1, $tv), $t1)];
},
- EApp::class => function () use ($env, $envMap) {
- throw new Exception('not implemented');
+ 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);
- $t1 = generalize(apply($s1, $env), $t1);
- $env = new TypeEnv(Map::insert($n, $t1, $envMap));
- [$s2, $t2] = ti($env, $e2);
+ $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 = 'example\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 \example\Map $env
- * @param Exp $e
+ * @param \example\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
+ * @param Type $t
* @return mixed
* @throws \Widmogrod\Useful\PatternNotMatchedError
*/
}
/**
- * @param Type $t
+ * @param Type $t
* @return mixed
* @throws \Widmogrod\Useful\PatternNotMatchedError
*/
return match([
ELit::class => match([
LInt::class => identity,
- LBool::class => identity,
+ LBool::class => function ($val) {
+ return $val ? 'true' : 'false';
+ },
]),
EVar::class => function ($n) {
return $n;
/**
* @dataProvider provideExamples
*/
- public function test(Exp $expression, $expected)
+ public function test(Exp $expression, $expected, $error = null)
{
- echo showImpl($expression), "\n";
+ // 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));
'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 EAbs("x", new EVar("x")),
new EVar("id")
),
- 'expected' => '(a1 -> a1)',
+ '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)',
],
-// // 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' => 'a3 -> a3',
-// ],
-// // 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(
-// 'x',
-// new EAbs(
-// 'x',
-// new ELet(
-// 'y',
-// new EVar('x'),
-// new EVar('y')
-// )
-// ),
-// new EApp(
-// new EVar('id'),
-// new EVar('id')
-// )
-// ),
-// 'expected' => 'a3 -> a3',
-// ],
-// // 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' => 'error: occur check fails: a0 vs. a0 -> a1',
-// ],
-// // 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 -> a1) -> a1',
-// ],
-// // e6 = EApp (ELit (LInt 2)) (ELit (LInt 2))
-// '(2 2)' => [
-// 'expression' => new EApp(
-// new ELit(new LInt(2)),
-// new ELit(new LInt(2))
-// ),
-// 'expected' => 'error: types do not unify: Int vs. Int -> a0',
-// ],
// 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' => 'error: unbound variable: y',
-// ],
+ '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',
+ ],
];
}
}
projects / php-functional.git / commitdiff
