Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
399fad4d
Commit
399fad4d
authored
Nov 11, 2020
by
Mickael Laurent
Browse files
comment previous 'new systems' and add rules for the declarative system
parent
c274a79b
Changes
2
Hide whitespace changes
Inline
Side-by-side
main.tex
View file @
399fad4d
...
...
@@ -335,24 +335,29 @@ The authors thank Paul-André Melliès for his help on type ranking.
\section
{
A crack to Flow Analysis
}
\label
{
app:flowanalysis
}
\input
{
flowanalysis
}
\newpage
%
\newpage
\section
{
New typecase system
}
\input
{
typecase
}
%
\section{New typecase system}
%
\input{typecase}
\newpage
%
\newpage
\section
{
New function refinement rules
}
\input
{
refining2
}
%
\section{New function refinement rules}
%
\input{refining2}
\newpage
%\newpage
%\section{Full new system with normal form}
%\input{new_system}
%\newpage
\section
{
Full new system with normal form
}
\input
{
new
_
system
}
%
\section{Full new system with normal form
(experimentation)
}
%
\input{new_system
2
}
\newpage
\section
{
Full n
ew system with normal form
(experimentation)
}
\input
{
new
_
system
2
}
\section
{
N
ew system with normal form
}
\input
{
new
_
system
3
}
\end{document}
new_system3.tex
0 → 100644
View file @
399fad4d
\subsection
{
Syntax
}
\[
\begin
{
array
}{
lrcl
}
\textbf
{
Types
}
&
t
&
::
=
&
b
\alt
t
\to
t
\alt
t
\times
t
\alt
t
\vee
t
\alt
\neg
t
\alt
\Empty
\end
{
array
}
\]
\begin{equation}
\label
{
expressions2
}
\begin{array}
{
lrclr
}
\textbf
{
Atomic expr
}
&
a
&
::=
&
c
\alt
x
\alt\lambda
x:t.e
\alt
(x,x)
\alt
x x
\alt
\tcase
{
x
}{
t
}{
e
}{
e
}
\alt
\pi
_
i x
\\
[.3mm]
\textbf
{
Expressions
}
&
e
&
::=
&
\letexp
{
x
}{
a
}{
e
}
\alt
a
\\
[.3mm]
\textbf
{
Values
}
&
v
&
::=
&
c
\alt\lambda
x:t.e
\alt
(v,v)
\\
\end{array}
\end{equation}
TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
\subsection
{
Declarative type system
}
\begin{mathpar}
\Infer
[Const]
{
}
{
\Gamma\vdash
c:
\basic
{
c
}}
{
}
\quad
\Infer
[Var]
{
}
{
\Gamma
\vdash
x:
\Gamma
(x)
}
{
x
\in\dom\Gamma
}
% \qquad
% \Infer[Inter]
% { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 }
% { \Gamma \vdash e: t_1 \wedge t_2 }
% { }
\\
\Infer
[Proj]
{
\Gamma
\vdash
x:
\pair
{
t
_
1
}{
t
_
2
}}
{
\Gamma
\vdash
\pi
_
i x:t
_
i
}
{
}
\qquad
\Infer
[Pair]
{
\Gamma
\vdash
x
_
1:t
_
1
\and
\Gamma
\vdash
x
_
2:t
_
2
}
{
\Gamma
\vdash
(x
_
1,x
_
2):
\pair
{
t
_
1
}
{
t
_
2
}}
{
}
\\
\Infer
[App]
{
\Gamma
\vdash
x
_
1:
\arrow
{
t
_
1
}{
t
_
2
}
\quad
\Gamma
\vdash
x
_
2: t
_
1
}
{
\Gamma
\vdash
{
x
_
1
}{
x
_
2
}
: t
_
2
}
{
}
\\
\Infer
[Case]
{
\Gamma\vdash
x:t
_
\circ\\
\Gamma\subst
{
x
}{
t
_
\circ\land
t
}
\vdash
e
_
1:t'
\\
\Gamma\subst
{
x
}{
t
_
\circ\land
\neg
t
}
\vdash
e
_
2:t'
}
{
\Gamma\vdash
\tcase
{
x
}
t
{
e
_
1
}{
e
_
2
}
: t'
}
{
}
\\
\Infer
[Abs]
{
\Gamma
,(x:s)
\vdash
e:t
}
{
\Gamma\vdash\lambda
x:s.e: t
}
{
}
\qquad
\Infer
[Let]
{
\Gamma\vdash
a:t
_
\circ\\
\Gamma
,(x:t
_
\circ
)
\vdash
e:t
}
{
\Gamma\vdash\letexp
x a e : t
}
{
}
\end{mathpar}
\begin{mathpar}
\Infer
[Subs]
{
\Gamma
\vdash
e:t
\\
t
\leq
t'
}
{
\Gamma
\vdash
e: t'
}
{
}
\qquad
\Infer
[Efq]
{
\exists
x
\in\dom
{
\Gamma
}
.
\ \Gamma
(x)=
\Empty
}
{
\Gamma
\vdash
e: t
}
{
}
\\
\Infer
[Split]
{
\Gamma
, (x:t
_
1)
\vdash
e: t
\\
\Gamma
, (x:t
_
2)
\vdash
e: t
\\
}
{
\Gamma
, (x:t
_
1
\vee
t
_
2)
\vdash
e: t
}
{
}
\Infer
[AbsSplit]
{
\Gamma\vdash
\lambda
x:s
_
1.
\
e: t
_
1
\\
\Gamma\vdash
\lambda
x:s
_
2.
\
e: t
_
2
\\
}
{
\Gamma\vdash
\lambda
x:s
_
1
\vee
s
_
2.
\
e: t
_
1
\wedge
t
_
2
}
{
}
\end{mathpar}
TODO: Inter rule needed?
\newpage
\subsection
{
Algorithmic type system
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment