07 Introduction to dependent types¶
This is a written summary of a presentation for BCS on the 29th of March 2022.
Main thread: dependent type for pratical purposes / industry
Goal of dependent types:
- Avoid mistakes
- Constrain programs
- Prove things
Benefits:
- Informative types
- Informative errors
- Interactive editing
Avoiding mistakes¶
Find the bug in this program
first of list
In Idris this would be a type error
Constrain programs¶
Here we can call this API with an empty string
DateFormat format = new SimpleDataFormat("")
But in idris this would be a type error
main = let myFormat = Main.fromString "yyyy/MM/dd"
in printLn myFormat
Error:
While processing right hand side of main. Can't find an implementation for StringFormat "".
Prove things¶
find an API where you just did something but you still have to check for it
Additional benefits¶
- Informative types
- Informative errors
- Interactive editing
Informative types¶
Server API in the type CLI options in the type
Informative errors¶
Show example of unhelpful errors
Show exmaple of helpful error
Interactive editing¶
Show type-at Show jump to definition Show skeleton definition Show expression search Show module browsing
My research: Servers and dependent types¶
write the type and the the server write the server and then infer the type write the description and generate the server