Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add type system #13

Merged
merged 22 commits into from
Aug 27, 2017
Merged
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
c97303c
Improve error propagation. Move functions out of eval case statement
smpoulsen Aug 11, 2017
b53286c
Move quote to own function. Add prelude/prelude
smpoulsen Aug 11, 2017
b16efbc
Initial HM type inference implementation
smpoulsen Aug 16, 2017
7ecaba8
Clean up unused variables; add type checking tests
smpoulsen Aug 16, 2017
fe46fa1
Add check for let expressions
smpoulsen Aug 16, 2017
18bd603
Fix type for built-in equal?
smpoulsen Aug 16, 2017
4a8a1d1
Type check ifs and booleans
smpoulsen Aug 16, 2017
9d35b3c
Fix substitution for inferring types in defined functions
smpoulsen Aug 17, 2017
4348e78
Inference for recursive functions
smpoulsen Aug 17, 2017
87b849e
Fix inference for if statements
smpoulsen Aug 17, 2017
f0080b5
Type check lists
smpoulsen Aug 18, 2017
3258428
Refactor list type unification
smpoulsen Aug 19, 2017
8efcf94
Remove threaded state for type var generation
smpoulsen Aug 19, 2017
e8528e5
Add inference for car, cdr, and cons
smpoulsen Aug 19, 2017
4be8bae
Propagate type errors throughout inference functions
smpoulsen Aug 19, 2017
da5d53f
Fix checking for letrec, add check for empty?
smpoulsen Aug 20, 2017
66dea40
Add additional type checking helpers
smpoulsen Aug 24, 2017
266ff17
Sub type environment through infer operands
smpoulsen Aug 24, 2017
a0a5875
wip working on letrec inference
smpoulsen Aug 25, 2017
d9ecc37
wip on letrec still; refactoring to separate constraint generaration
smpoulsen Aug 25, 2017
a41b818
Functional inference for recursive, higher order functions
smpoulsen Aug 26, 2017
28baa8e
Refresh type variables after finishing inference
smpoulsen Aug 27, 2017
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
wip working on letrec inference
Almost right; just getting two variables that should be different
  • Loading branch information
smpoulsen committed Aug 25, 2017
commit a0a58751057fc578c7dfab554dd011aa7eff9696
43 changes: 33 additions & 10 deletions lib/types/type_evaluator.ex
Original file line number Diff line number Diff line change
Expand Up @@ -164,11 +164,16 @@ defmodule Terp.Types.TypeEvaluator do
infer(bound, type_env)
:__letrec ->
# TODO not inferring the specific type
[_name | [bound | []]] = operands
[name | [bound | []]] = operands
tv = TypeVars.fresh()
{s1, t1} = {null_substitution(), tv}
type_env = apply_sub(s1, type_env)
t1_prime = generalize(type_env, t1)
type_env = extend(type_env, {name.node, t1_prime})
with {:ok, {s1, t}} <- infer(bound, type_env),
tv = TypeVars.fresh(),
{:ok, s2} <- unify(Types.function(tv, tv), t) do
{:ok, {s2, apply_sub(s1, t)}}
require IEx; IEx.pry
{:ok, {s2, apply_sub(s1, tv)}}
else
{:error, e} -> {:error, e}
end
Expand Down Expand Up @@ -211,6 +216,7 @@ defmodule Terp.Types.TypeEvaluator do
substituted_type_vars = type_vars
|> Enum.reverse()
|> Enum.map(&apply_sub(s, &1))
require IEx; IEx.pry
{:ok, {s, build_up_arrows((substituted_type_vars ++ List.wrap(t)))}}
{:error, e} ->
{:error, e}
Expand All @@ -231,18 +237,34 @@ defmodule Terp.Types.TypeEvaluator do
# TODO filter our provide nodes
{:ok, {null_substitution(), nil}}
_ ->
t = TypeVars.fresh()
{:ok, {null_substitution(), t}}
{s1, t1} = case lookup(type_env, operator.node) do
{:ok, {s, t}} ->
{s, t}
{:error, _} ->
{null_substitution(), TypeVars.fresh()}
end

with {:ok, {type_env, {s2, ts}}} <- infer_operands(operands, apply_sub(s1, type_env)),
tv = TypeVars.fresh(),
fn_type = build_up_arrows(Enum.reverse([tv | ts])),
{:ok, s3} <- unify(apply_sub(s2, t1), fn_type) do
composed_scheme = compose(s3, compose(s2, s1))
require IEx; IEx.pry
{:ok, {composed_scheme, apply_sub(s3, tv)}}
else
{:error, e} ->
{:error, e}
end
end
_ ->
lookup(type_env, node)
end
end

def infer_operands(operands, type_env) do
Enum.reduce(operands, {type_env, {%{}, []}},
Enum.reduce(operands, {:ok, {type_env, {%{}, []}}},
fn (_expr, {:error, _} = error) -> error
(expr, {t_env, {sub, types}}) ->
(expr, {:ok, {t_env, {sub, types}}}) ->
case infer(expr, t_env) do
{:ok, {sub_prime, type}} ->
subbed_env = apply_sub(sub_prime, type_env)
Expand Down Expand Up @@ -336,10 +358,11 @@ defmodule Terp.Types.TypeEvaluator do
@doc """
Generalize a bound type
"""
@spec generalize(type_environment, Types.t) :: scheme
def generalize(type_env, type) do
xs = type
|> MapSet.difference(ftv(type_env))
|> ftv()
|> MapSet.difference(ftv(type_env))
|> MapSet.to_list()
{xs, type}
end
Expand Down Expand Up @@ -374,7 +397,7 @@ defmodule Terp.Types.TypeEvaluator do
{as, t_prime}
end
def apply_sub(substitution, xs) when is_list(xs) do
Enum.map(xs, &apply(substitution, &1))
Enum.map(xs, &apply_sub(substitution, &1))
end
def apply_sub(substitution, %{} = type_env) do
type_env
Expand All @@ -393,7 +416,7 @@ defmodule Terp.Types.TypeEvaluator do
MapSet.union(ftv(t1), ftv(t2))
end
def ftv({as, type}) do
ftv(MapSet.difference(type, MapSet.new(as)))
MapSet.difference(ftv(type), MapSet.new(as))
end
def ftv(xs) when is_list(xs) do
Enum.reduce(xs, MapSet.new(), fn (x, acc) -> MapSet.union(ftv(x), acc) end)
Expand Down