3This paper documents a new implementation of \Idris{}~\cite{Brady2011a}, in which
4I attempt to learn from the mistakes of the previous implementation and make
5it nice and clean and solid. Maybe I'll keep it up to date as I write the
8The title is deliberately a reordering of the words in my thesis
9title~\cite{Brady2005}. Whereas that was about taking elaborated programs
10in the core type theory of \Epigram{}~\cite{McBride2004a} and compiling them
11efficiently (i.e. making the language implementation practical) this paper is
12about making the language itself practical.
14\subsection{Some Goals}
17\item Type checking dependent types~\cite{Chapman2005epigram,loh2010tutorial} is just one component
18 of a language. There is folklore about what to do to turn it into a language. This
19 paper aims to help language implementers avoid working things out for themselves.
20\item What's the difference between a theorem prover and a practical systems programming
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list