Skip to content

Commit

Permalink
Move the poly_2 test functions to should_fail
Browse files Browse the repository at this point in the history
All these function coming from the paper "Bidirectional Typing
for Erlang" (N. Rajendrakumar, A. Bieniusa, 2021) require
higher-rank (at least rank-2) polymorphism. To be able to
have higher-ranked polymorphism, we would have to be able to
express inner quantifiers. We don't have that in the typespec
syntax, so the traditional way of interpreting type variables
in specs is to treat them all as quantified at the top-level.

Authors of the paper took a non-standard approach, to quote it:

    Type specifications in Erlang consider all type variables
    as universal and thus restrict the types to prefix or rank-1
    polymorphism.

    For allowing higher-rank polymorphism, we are interpreting
    the type specification differently, namely we are adding
    the quantifier to the type variable with the smallest scope.

    -spec poly_2(fun((A) -> A)) -> {boolean(), integer()}.

    For example, the type spec for function poly_2 above is
    interpreted as
        (∀a.(a) → a) → {boolean(), integer()}
    instead of
        ∀a.((a → a) → {boolean(), integer()})

I argue that this interpretation of type variables would
be confusing for users. Additionally, I think that there
is not much value in having higher-rank polymorphism in
a dynamically/gradually typed language. In Haskell, it
is useful for sure (even though one does not encounter
it very often) but this is because there is a strict
typechecker that doesn't accept anything you cannot type
well. Here, in Erlang, if you ever come to a situation
where you need higher-rank polymorphism (and I think it
is quite unlikely), you can always fallback to any().
  • Loading branch information
xxdavid committed Jan 22, 2024
1 parent 719dbab commit d8125c9
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 11 deletions.
10 changes: 9 additions & 1 deletion test/should_fail/poly_fail.erl
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@
%% See "Bidirectional Typing for Erlang", N. Rajendrakumar, A. Bieniusa, 2021, Section 2. Examples.
-export([find1/0,
poly_2/1,
poly_fail/3]).
poly_2b/1,
poly_fail/3,
poly_fail_2/3]).

%% These examples don't come from the above paper.
-export([f/1,
Expand All @@ -25,9 +27,15 @@ find1() ->
-spec poly_2(fun((A) -> A)) -> {integer(), boolean()}.
poly_2(F) -> {F(42), F(false)}.

-spec poly_2b(fun((A) -> A)) -> {integer(), integer()}.
poly_2b(F) -> {F(42), F(84)}.

-spec poly_fail(fun((A) -> A), boolean(), integer()) -> {boolean(), integer()}.
poly_fail(F, B, I) -> {F(I), F(B)}.

-spec poly_fail_2(fun((A) -> A), boolean(), boolean()) -> {boolean(), boolean()}.
poly_fail_2(F, B1, B2) -> {F(B2), F(B1)}.

-spec f([integer(), ...]) -> atom().
f(L) ->
hd(L).
Expand Down
10 changes: 0 additions & 10 deletions test/should_pass/poly_pass.erl
Original file line number Diff line number Diff line change
@@ -1,21 +1,11 @@
-module(poly_pass).

%% See "Bidirectional Typing for Erlang", N. Rajendrakumar, A. Bieniusa, 2021, Section 2. Examples.
-export([poly_2/1,
poly_pass/3]).

%% These examples don't come from the above paper.
-export([f/1,
l/0]).

-gradualizer([solve_constraints]).

-spec poly_2(fun((A) -> A)) -> {integer(), integer()}.
poly_2(F) -> {F(42), F(84)}.

-spec poly_pass(fun((A) -> A), boolean(), boolean()) -> {boolean(), boolean()}.
poly_pass(F, B1, B2) -> {F(B2), F(B1)}.

-spec f([integer(), ...]) -> integer().
f(L) ->
hd(L).
Expand Down

0 comments on commit d8125c9

Please sign in to comment.