Skip to content

Commit 9679c55

Browse files
authored
Refactor
1 parent 64b3db7 commit 9679c55

22 files changed

+2383
-1420
lines changed

README.md

Lines changed: 31 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,26 @@
11
# Typelixir
22

3-
**TODO: Add description**
3+
The library proposes a type system that makes possible to perform static type-checking on a significant fragment of Elixir.
4+
5+
An important feature of the type system is that it does not require any syntactic change to the language. Type information is provided by means of function signatures `@spec`.
6+
7+
The approach is inspired by the so-called [gradual typing](https://en.wikipedia.org/wiki/Gradual_typing).
8+
9+
The proposed type system is based on subtyping and is backwards compatible, as it allows the presence of non-typed code fragments. Represented as the `any` type.
10+
11+
The code parts that are not statically type checked because of lack of typing information, will be type checked then at runtime.
12+
13+
[Here](./lib/TYPE_SYSTEM.md) is the proposed type system and how to write the code to be statically type checked.
14+
15+
### Note
16+
17+
The library is not extensive within the language. The scope of this work is to cover the expectations of a degree project for the [Facutlad de Ingeniería - UDELAR](https://www.fing.edu.uy/).
18+
19+
Special thanks to our tutors Marcos Viera and Alberto Pardo.
20+
21+
## Documentation
22+
23+
Documentation can be found at [https://hexdocs.pm/typelixir](https://hexdocs.pm/typelixir).
424

525
## Installation
626

@@ -15,7 +35,14 @@ def deps do
1535
end
1636
```
1737

18-
Documentation can be generated with [ExDoc](https://github.com/elixir-lang/ex_doc)
19-
and published on [HexDocs](https://hexdocs.pm). Once published, the docs can
20-
be found at [https://hexdocs.pm/typelixir](https://hexdocs.pm/typelixir).
38+
After installing the dependency, you need to run:
39+
40+
```bash
41+
mix typelixir
42+
```
43+
44+
## License
45+
46+
typelixir is licensed under the MIT license.
2147

48+
See [LICENSE](./LICENSE) for the full license text.

lib/TYPE_SYSTEM.md

Lines changed: 302 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,302 @@
1+
# Typed Elixir
2+
3+
## Introduction
4+
5+
Elixir posseses some basic types such as `integer`, `float`, `string`, `boolean` and `atom` which are dynamically type checked at runtime.
6+
7+
The aim of this library is to introduce a type system in order to perform static typing on expressions of both basic types and structured types. Besides the basic types, our type system manipulates types for `lists`, `tuples`, `maps` and `functions`. We also include the type `any` as the supertype of all terms, and `none` as the empty type.
8+
9+
Below there are some examples of how the library type check the code (but they are not extensive to all use cases, so if in doubt, give it a try!).
10+
11+
## Structured types
12+
13+
Heterogeneous lists are not allowed. The following list generates a type error:
14+
15+
```elixir
16+
[1, "two", :three ] # wrong
17+
```
18+
19+
Only homogeneous lists are allowed, like the following ones:
20+
21+
```elixir
22+
[1, 2, 3] # list of integer
23+
[[1, 2], [3, 4], [5, 6]] # list of integers lists
24+
```
25+
26+
For maps, all keys must have the same type but each value can have its own type:
27+
28+
```elixir
29+
%{:age => 12, name: "John" } # map with atom keys
30+
%{1 => 12, name: => "John" } # wrong
31+
```
32+
33+
For tuples, each element has its own type:
34+
35+
```elixir
36+
{12, "John"} # duple where the first element is an integer and the second a string
37+
```
38+
39+
Last, integer type can be used as float because it is a subtype of it:
40+
41+
```elixir
42+
[1, 1.5, 2] # list of float
43+
%{1 => "one", 1.5 => "one dot five" } # map with float keys
44+
```
45+
46+
## Expressions
47+
48+
For boolean expressions like `and`, `or` and `not` boolean types are expected:
49+
50+
```elixir
51+
true and false # false
52+
true and (0 < 1) # true
53+
true or 1 # wrong
54+
```
55+
56+
In the case of comparison operators we are more flexible, following Elixir's philosophy. We allow any value even of different types to be compared with each other. However, the return type is always boolean. Therefore:
57+
58+
```elixir
59+
("hi" > 5.0) or false # true
60+
("hi" > 5.0) * 3 # wrong
61+
```
62+
63+
For `case` sentences, the expression in the case has to have the same type as the guards, and the return type of all guards must have the same type:
64+
65+
```elixir
66+
case 1 > 0 do
67+
true -> 1
68+
false -> 1.5
69+
end # 1
70+
71+
case 1 + 2 do
72+
2 -> "This is wrong"
73+
3 -> "This is right"
74+
end # "This is right"
75+
76+
case 1 + 2 do
77+
"tres" -> "This is wrong"
78+
3 -> "This is right"
79+
end # wrong
80+
81+
case 1 + 2 do
82+
1 -> :wrong
83+
3 -> "This is right"
84+
end # wrong
85+
```
86+
87+
The behavior for `if` and `unless` is the same and for the `cond` sentence, a boolean condition is expected always on each guard.
88+
89+
## Function specifications
90+
91+
The library uses the reserved word `@spec` for functions specs.
92+
93+
It doesn't type check functions defined with `when` conditions, they will be checked at runtime as Elixir does.
94+
95+
One of the main objectives of the design of our type system is to be backward compatible to allow working with legacy code. To do so, we allow the existence of `untyped functions`.
96+
We can also see them as functions that doesn't have a `@spec` specification.
97+
98+
In the following example we define a function that takes an integer and returns a float:
99+
100+
``` elixir
101+
@spec func1(integer) :: float
102+
def func1(x) do
103+
x * 42.0
104+
end
105+
```
106+
107+
Function `func1` can be correctly applied to an integer:
108+
109+
```elixir
110+
func1(2) # 84.0
111+
```
112+
113+
But other kinds of applications will fail:
114+
115+
```elixir
116+
func1(2.0) # wrong
117+
func1("2") # wrong
118+
```
119+
120+
We can also define functions using the `any` type to avoid the type check:
121+
122+
```elixir
123+
@spec func2(any) :: boolean
124+
def func2(x) do
125+
x == x
126+
end
127+
```
128+
129+
All types are subtype of this one, so this function can be called with any value:
130+
131+
```elixir
132+
func2(1) # true
133+
func2("one") # true
134+
func2([1, 2, 3]) # true
135+
```
136+
137+
If we want to specify a function with a list of integers as parameter we write:
138+
139+
```elixir
140+
@spec func3([integer]) :: integer
141+
def func3([]) do
142+
0
143+
end
144+
145+
def func3([head|tail]) do
146+
1 + func3(tail)
147+
end
148+
```
149+
150+
This function can be called:
151+
152+
```elixir
153+
func3([]) # 0
154+
func3([1, 2, 3]) # 3
155+
156+
func3(["1", "2", "3"]) # wrong
157+
func3([:one, :two, :three]) # wrong
158+
func3([1, :two, "three"]) # wrong
159+
```
160+
161+
Note that the empty list can be used as a list of any type.
162+
163+
Also, we can define a function applicable to all list types using the `any` type:
164+
165+
```elixir
166+
@spec func4([any]) :: integer
167+
def func4([]) do
168+
0
169+
end
170+
171+
def func4([head|tail]) do
172+
1 + func4(tail)
173+
end
174+
```
175+
176+
So now we can have `func4` calls like the following:
177+
178+
```elixir
179+
func4([]) # 0
180+
func4([1, 2, 3]) # 3
181+
func4(["1", "2", "3"]) # 3
182+
func4([:one, :two, :three]) # 3
183+
184+
func4([1, :two, "three"]) # wrong
185+
```
186+
187+
A map with more key-value pairs can be used instead of a map with less entries. The next function is applicable to maps that have at least one key-value pair, with atom keys and the first value has atom type:
188+
189+
```elixir
190+
@spec func5(%{atom => atom}) :: boolean
191+
def func5(map) do
192+
map[:key1] == :one
193+
end
194+
```
195+
196+
So this function can be called with:
197+
198+
```elixir
199+
func5(%{:key1=>:three, :key2=>:three, :key3=>"three"}) # false
200+
func5(%{:key1=>:one, :key2=>:two, :key3=>"three"}) # true
201+
202+
func5(%{"1"=>:one, "two"=>:two}) # wrong -> keys are not atoms
203+
func5(%{:key1=>:one, "two"=>:two, 3=>:three}) # wrong -> keys have different types
204+
func5(%{}) # wrong -> has less key-value pairs
205+
```
206+
207+
If we want to specify a function that takes a map with any key type as param we can use the `none` type because, as it is usual, maps are `covariant` on its key and we have to use the lower type. We can also say that the first elem has to have type `any` to admit maps with any value types:
208+
209+
```elixir
210+
@spec func6(%{none => any}) :: boolean
211+
def func6(map) do
212+
map[:key1] == :one
213+
end
214+
```
215+
216+
Some invocations to this function are:
217+
218+
```elixir
219+
func6(%{"one"=>:one, "two"=>2, "three"=>"three"}) # false
220+
func6(%{"one"=>1, "two"=>2, "three"=>3}) # false
221+
func6(%{:key1=>:one, :key2=>2, :key3=>"three"}) # true
222+
func6(%{:key1=>:one, :key2=>:two, :key3=>:three}) # false
223+
224+
func6(%{1=>:one, :two=>2, "three"=>"three"}) # wrong -> keys have different types
225+
func6(%{}) # wrong -> has less key-value pairs
226+
```
227+
228+
### Return types
229+
230+
If we don't want to specify the return type we can denote it as `any`:
231+
232+
```elixir
233+
@spec func8([any]) :: any
234+
def func8(list) do
235+
[head | tail] = list
236+
head
237+
end
238+
```
239+
240+
This function can be called as:
241+
242+
```elixir
243+
func8(["one", "two", "three"]) # "one"
244+
func8([1, 2, 3]) # 1
245+
func8([:one, :two, :three]) # :one
246+
func8([[1,2,3], [4,5,6], [7,8,9]]) # [1,2,3]
247+
```
248+
249+
As we did for parameters, we can specify that the return type is a list of any type:
250+
251+
```elixir
252+
@spec func9([any]) :: [any]
253+
def func9(list) do
254+
[head | tail] = list
255+
tail
256+
end
257+
```
258+
259+
Some examples of usage are:
260+
261+
```elixir
262+
func9([1]) # []
263+
func9([1,2]) # [2]
264+
func9([1.1, 2.0]) # [2.0]
265+
func9(["one", "two", "three"]) # ["two", "three"]
266+
func9([:one, :two]) # [:two]
267+
func9([{1,"one"}, {2,"two"}, {3,"three"}]) # [{2,"two"}, {3,"three"}]
268+
func9([%{1 => 3}, %{2 => "4"}, %{3 => :cinco}]) # [%{2 => "4"}, %{3 => :cinco}]
269+
```
270+
In the same way, this behavior can be obtained for maps and tuples.
271+
272+
### Runtime errors
273+
274+
Expressions with `any` type can be used anywhere so we could have:
275+
276+
```elixir
277+
func3(func9([0,1])) # 2
278+
func3(func9(['a', 'b'])) # runtime error
279+
```
280+
281+
Statically both functions are correctly type checked but dynamically the second one will fail.
282+
283+
As we mentioned before, functions without type specification have the same behaviour. For example, the following expression type checks correctly:
284+
285+
```elixir
286+
id(8) + 10 # 18
287+
```
288+
289+
But the following will fail at runtime:
290+
291+
```elixir
292+
"hello" <> Main.fact(9) # runtime error
293+
id(8) and true # runtime error
294+
```
295+
296+
## Closing thoughts
297+
298+
We strongly believe that there's a lot of room for further research and improvement of the language in this area.
299+
300+
The library is not extensive to all the language, we are missing some important operators such as `|>` or the mentioned `when`.
301+
302+
It's a proof of concept, the scope of this work is just to cover the expectations of a degree project.

lib/example/foo.ex

Lines changed: 0 additions & 3 deletions
This file was deleted.

lib/mix/tasks/typelixir.ex

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,11 @@ defmodule Mix.Tasks.Typelixir do
1111
end
1212

1313
defp get_paths() do
14-
paths = Mix.Project.config()[:elixirc_paths] |> Mix.Utils.extract_files([:ex])
14+
paths =
15+
Mix.Project.config()[:elixirc_paths]
16+
|> Mix.Utils.extract_files([:ex])
1517

16-
IO.puts "\nTypelixir -> Compiling #{length(paths)} #{if (length(paths) > 1), do: "files", else: "file"} (.ex)\n"
18+
IO.puts "\nTypelixir -> Compiling #{length(paths)} file#{if (length(paths) > 1), do: "s"} (.ex)\n"
1719
paths
1820
end
1921
end

0 commit comments

Comments
 (0)