forked from idris-lang/Idris-dev
-
Notifications
You must be signed in to change notification settings - Fork 0
/
conclusions.tex
34 lines (23 loc) · 1.3 KB
/
conclusions.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
\section{Discussion}
\label{sect:discussion}
Since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it makes
sense to expose the tactic language to the programmer.
Also tactic-implicit arguments as a generalisation of instance resolution.
Discuss performance (anecdotally, how big is the library and how long to check,
and relative to previous version).
\subsection{Related Work}
Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.
How does Agda~\cite{norell2007thesis} work?
Earlier \Idris{}, with \Ivor{}~\cite{Brady2006b}.
Comparison with GHC's type system and type checker.
\subsection{Conclusion}
[Observation: separate elaboration and type checking, sort of like in GHC which
type checks the high level language and produces a type correct core language.
Elaboration is effectively a type checker for the high level language, so we have
a hope of providing reasonable error messages related to the original code.]
\subsection{Further Work}
[Would the EDSL approach work in other languages? Adding components of DTP
to imperative languages, say, using \TT{} as a verified core.
\Idris{} implementation as the beginning of a project to explore practical
DTP --- systems, protocols, security especially. And just having full
dependent types for lightweight correctness guarantees.]