Реализация Файловой системы на языке Idris

Требуется разработать прототип файловой системы на зависимых типах на языке Idris 2 Обязательно использование зависимых типов, следовательно все проверки на этапе компиляции...