Skip to content

Latest commit

 

History

History
12 lines (10 loc) · 972 Bytes

README.md

File metadata and controls

12 lines (10 loc) · 972 Bytes

SKITypes

Implementing the SKI combinator calculus in Haskell's type system

skiType.hs is an experiment to implement a Turing-complete programming language in Haskell's type system. The idea is to create a functional dependency between two types, say x and y such that x reduces to y. If x and y are composed of the SKI combinators and the reduction rules are the rules of the SKI combinator calculus, then you should be able to "calculate" y by typechecking a function of type x -> y when applied to a value of the type x. That's essentially what skiType.hs does!

skiValue.hs is an implementation of SKI on the value level. You can compare the two reductions to see how they follow the same logic.