Idris

Idris 係一隻純函數式程式語言，具有依賴類型、可以揀嘅惰性求值仲有整體檢查器等嘅功能。Idris 通常畀人攞嚟做證明助手，但佢喺設計嗰陣諗住攞嚟做類似於 Haskell 嘅通用編程語言。