Specification for Typespecs Encoding in Core Erlang?

Questions / Help
,
1

I am trying to understand how Erlang typespecs are encoded in Core Erlang and would like to find some information.

I consulted the Core Erlang specification, but as far as I can tell, typespecs are not discussed. This tutorial and paper do not refer to typespecs either.

Compiling the following Erlang module, simple.erl,

-module(simple).

-export([double/1, wrap/1]).

-type datum() :: integer() | float() | atom(). 

-spec double(integer() | float()) -> float().
double(A) -> A * 2.0.

-spec wrap(A)-> {a, A} when A :: datum().
wrap(A) -> {a, A}.

to Core Erlang (erlc +to_core simple.erl) yields the following:

module 'simple' 
	['double'/1, 'wrap'/1]

attributes [
	'type' =
		[{'datum',{'type',{5,18},'union',[{'type',{5,18},'integer',[]}|[{'type',{5,30},'float',[]}|[{'type',{5,40},'atom',[]}]]]},[]}],
	'spec' =
		[{{'double',1},[{'type',{7,13},'fun',[{'type',{7,13},'product',[{'type',{7,14},'union',[{'type',{7,14},'integer',[]}|[{'type',{7,26},'float',[]}]]}]}|[{'type',{7,38},'float',[]}]]}]}],
	'spec' =
		[{{'wrap',1},[{'type',{10,11},'bounded_fun',[{'type',{10,11},'fun',[{'type',{10,11},'product',[{'var',{10,12},'a'}]}|[{'type',{10,17},'tuple',[{'atom',{10,18},'a'}|[{'var',{10,21},'a'}]]}]]}|[[{'type',{10,29},'constraint',[{'atom',{10,29},'is_subtype'}|[[{'var',{10,29},'a'}|[{'user_type',{10,34},'datum',[]}]]]]}]]]}]}]
	]

'double'/1 =
	fun (_0) -> call 'erlang':'*'(_0, 2.00000000000000000000e+00)

'wrap'/1 =
	fun (_0) -> {'a', _0}
end

The user-defined datum() type is encoded as the key-value pair 'type' = [...] in the attributes list, as are the typespecs for double/1 and wrap/1. Is there any existing specification for translating Erlang typespecs into such an encoding?

1 Like
2

Not as far as I can remember, no! The thing to remember is that the typespecs aren’t actually used by the compiler at all. The compiler completely ignores them and all it does are some simple checks on the syntax. Erlang is dynamically typed and all type checking is done at runtime and mainly in the BEAM. When you add two things together the plus operator in the BEAM at runtime checks whether they are numbers.

This means that the typespecs can be completely wrong and it will make no difference to the generated code. You can define a function which takes a tuple as argument and it returns an atom but typespec it as taking an integer argument and returning a list and the compiler accepts this and uses the code to work on. The code is the actual source of truth.

So why do typespecs? One good reason is for documentation, and another good reason is for type checking programs like dialyzer.

9 Likes
3

Thanks for your detailed explanation about typespecs.

The reason behind my question about them is to see how difficult it would be to use the corresponding encoding of typespecs in Core Erlang. Our idea would be to use Core Erlang as an intermediate language over which a type-checking pass is performed. For this reason, we would need to extract the typespec information from Core Erlang, if that makes sense.

1 Like
4

Why would you want to use Core Erlang as an intermediate language and not Erlang

1 Like
5

The encoding of types is described in the documentation of the the abstract format in the section Types.

1 Like
6

But note that this is for the Erlang AST and not Core erlang!

1 Like
7

After all, we decided to follow a different route and use the abstract Erlang syntax instead of Core Erlang, as you suggested.

2 Likes