>>8775402To compare with Haskell, pic related is an example from the idris book (all the code can be downloaded in the book link above)
Basically, you have a boolean data type
>B={True, False}(called DoorState={DoorOpen,DoorClosed} here)
and a door command type, essentially
>DoorCmd : B -> B -> Typewhich let's you construct 4 types
namely
>DoorCmd(DoorOpen,DoorOpen)>DoorCmd(DoorOpen,DoorClosed)>DoorCmd(DoorClosed,DoorOpen)>DoorCmd(DoorClosed,DoorClosed)and then some monad stuff to set up "do" notation.
The gain is that you can e.g. write
my_program : DoorCmd(DoorClosed,DoorClosed)
and the code you write below won't compile unless it satisfies the specifications that all actions start out with a closed door and in the end you end up with a closed door again.
It's descibed in this chapter
https://manning-content.s3.amazonaws.com/download/7/b2efb6c-0182-47e4-a78b-797c49e66d0d/SampleCh13.pdfSince Intuitionistic type theory bascially IS constructive formal logic via Curry Howard, all mathematically thinkable specifications can be put into a type expression this way. Meaning e.g. your boss can write a few lines expressing a type that says
>map an integer to a (the) list of it's prime factors(i.e. the full specification of a task)
and the employee is now tasked to implement an algorithm, and his shit won't even compile unless it does exactly what it's supposed to. The whole spec has made it into the type system, because it's expressive as math itself.
And maybe we can automate programming in this way, to some extend, i.e. have programs generated, just having to write the type. Haskell can do this to some extend, where it's easy.
E.g. if you write the type
SwichType = forall a b. (a,b) -> (b,a)
then the Haskell compiler can compute an algorthm that fits the type (because there is only one function that has that type, extensionally speaking)
https://en.wikipedia.org/wiki/Intuitionistic_type_theoryhttps://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence 
