Skip to content

trillioneyes/dyn-universe

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

7 Commits
 
 
 
 
 
 

Repository files navigation

Fun with "Dynamic" Typing: An Introduction to Universes

This is a simple introduction to universes, a tool that can be used in dependently- typed languages to get all the convenience of dynamic types (often referred to in academia as "generic programming") from inside a strong static type system. My code is written in Idris, but this guide is aimed at people who know Haskell or OCaml but are new to dependent typing. (At least, I hope. If someone in the target audience finds something unclear, feel free to submit an issue!)

Using this tutorial

This tutorial contains a bunch of .md files. You can just read through them all if you like... but they are also valid "literate" idris files! That means if you download the raw files and change their extension to .lidr, you can run them directly in the idris repl (everything that's not code will be treated as a comment). You can use this to play with some of the examples, if you want.

About

Fun with "Dynamic" Typing: An Introduction to Universes

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages