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

feat: add recursion support #61

Conversation

polvalente
Copy link
Contributor

@polvalente polvalente commented Dec 13, 2020

The main functionality addition here is enabling the type checker to not hang upon recursions.

This was done by adding a Loop type which can then be used to properly warn the user about the recursion.

Support for inter-module loops still needs to be verified. In theory, this PR already supports it, but I found no easy way for testing this.

Also, I ended up adding a minor fix to the public_function_def combinator so it supports empty functions.

@polvalente polvalente force-pushed the feat/support-recursion-in-type-checker branch from 9997802 to 91484e9 Compare December 13, 2020 04:25
@polvalente polvalente force-pushed the feat/support-recursion-in-type-checker branch 2 times, most recently from 054a7dd to 76acf47 Compare December 13, 2020 13:34
@@ -90,6 +90,13 @@ defmodule Fika.Compiler.Parser.Types do
|> label("effect type")
|> Helper.to_ast(:effect_type)

loop_type =
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are still tests that need to be written for this. I mostly added it because I wanted to see if the module_compiler_test.exs suite would pass with the get_type refactor

:ok
end

def set(f, g) do
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of mapping {f, g}, ideally we should keep track of all the indirect dependencies so we can handle cases like a -> b -> c -> a

A data structure like the one below would solve this.

%{a: MapSet([b, c]), b: MapSet([c, a]), c: MapSet([b, a]}

to_atom("Nothing")
end

ext to_atom(x: String) : Nothing = {"Elixir.String", "to_atom", [x]}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@emilsoman I tried removing this, but to keep my Nothing test, I'll have to either introduce a Nothing literal or accept uppercase letters in atoms.

For now, I managed to introduce this lovely piece of code to force things

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This also shows that it may be better to accept :"<content>" syntax and also to support the same charsets as Elixir and Erlang support for atoms

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😄 haha i understand the pain here. We can support :"string" in the future

@polvalente polvalente changed the title feat: add recursion support to type checker feat: add recursion support Dec 14, 2020
{:ok, _} ->
:ok
Enum.each(state.unchecked_functions, fn {signature, function} ->
# We need to use this approach instead of Task.async_stream due to
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@emilsoman I had to roll this back because some tests were hanging. I've added this comment to make it clear why we take this approach

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, we can just say the tests were hanging and which ones as part of the comment to make it clearer

@@ -0,0 +1,34 @@
defmodule Fika.Compiler.CodeServer.FunctionDependencies do
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@emilsoman I ended up keeping this as a separate submodule because in this way we can use the same graph logic for handling loops in the sequential type checker version!

In that case, we initialize a separate graph which reference is propagated upwards in the callstack. I'll point the relevant pieces of code in the TypeChecker module

Comment on lines 486 to 487
|> Map.put(:latest_called_function, mfa)
|> Map.put_new(:callstack, FunctionDependencies.new_graph())
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whenever we start the callstack, we don't have the :callstack set, so we need to create a new dependency graph.
In a future refactor, we can use Env structs instead of plain maps, and force envs to have new graph by default.

Also, the first call in the stack will have :latest_called_function unset, so we currently check this to avoid touching an unset graph

end
result =
if latest_call = env[:latest_called_function] do
FunctionDependencies.set_function_dependency(
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For each subsequent call in the stack, we have both the mfa for the last called function and for the current one. This implies that :latest_called_function depends on mfa, so we can set this on the graph

@emilsoman
Copy link
Member

@polvalente I was spending some time on this the past few days and I think we should first define our expected behaviour. The following should type check successfully:

    fn a : Loop(Int | String) do
      if true do
        b()
      else
        123
      end
    end

    fn b : Loop(Int | String) do
      if true do
        c()
      else
        "abc"
      end
    end

    fn c : Loop(Int | String) do
      a()
    end

    fn d : Int | String do
      a()
    end

Also, note regarding functions with effects: currently if there's a function with a side effect, it's return type will be Effect(<some time>). If this function is recursive, it will be Loop(Effect(<some type>)). Here "Loop" and "Effect" are flags that indicate that the function is recursive and it has a side effect. This means Loop(Effect(<type>)) and Effect(Loop(<type>)) should be treated the same. While this is okay to get started with, I'm wondering if we should introduce some form of "flag" in the type signature, something like fn my_function(x: Int) : Int !effect !loop or fn my_function(x: Int) -[loop, effect]-> Intetc. Do you have any ideas for this?

@polvalente
Copy link
Contributor Author

@polvalente I was spending some time on this the past few days and I think we should first define our expected behaviour. The following should type check successfully:

    fn a : Loop(Int | String) do
      if true do
        b()
      else
        123
      end
    end

    fn b : Loop(Int | String) do
      if true do
        c()
      else
        "abc"
      end
    end

    fn c : Loop(Int | String) do
      a()
    end

    fn d : Int | String do
      a()
    end

Alright! I'll try to get this to work next week. Feel free to make your own attempts if you like, just let me know!

Also, note regarding functions with effects: currently if there's a function with a side effect, it's return type will be Effect(<some time>). If this function is recursive, it will be Loop(Effect(<some type>)). Here "Loop" and "Effect" are flags that indicate that the function is recursive and it has a side effect. This means Loop(Effect(<type>)) and Effect(Loop(<type>)) should be treated the same. While this is okay to get started with, I'm wondering if we should introduce some form of "flag" in the type signature, something like fn my_function(x: Int) : Int !effect !loop or fn my_function(x: Int) -[loop, effect]-> Intetc. Do you have any ideas for this?

I think that for this first iteration it's ok to return Loop(Effect(<type>)). However, it does seem nicer having function annotation flags instead of a a type wrapper, and even more so since they don't have precedence over each other (and even if we introduce ones that have, this can be documented outside of the annotations, just like operator precedence)

@polvalente
Copy link
Contributor Author

Closed in favor of #87

@polvalente polvalente closed this Mar 6, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants