Re:Talks that changed the way I think about programming
by chriswarbo on Thursday December 08, 2016 @08:14AM
(#13130056)
> I don't think it's practical, but it's the sort of thing that some person someday will incorporate in some more comfortable way in a new language or platform as a revolutionary feature.
As mentioned below, this can be used in languages like Agda and Idris; they also give you proof search, which tries to automatically fill in the holes from available definitions. This works well for 'proof objects' (the name given to values which only exist to satisfy the type checker), but requires caution for values with 'computational content' (those values which can effect the resulting computation).
Pretty much all Haskell code (except the really wacky astronautical stuff) has computational content, so there are fewer "obvious" obligations to fill in than would appear in a proof (in fact, due to laziness and lack of totality, we can safely use 'undefined' for all proof objects, since they'll never be pattern-matched!).
For example, if our function needs to return a list (e.g. if we're writing a function like map, filter, iterate, replicate, cycle, etc.), a proof search will immediately give us the empty list '[]', which is correctly typed but probably wrong.
For Haskell, tools like djinn can get you a little hole-filling automation, and I think that Emacs modes like ghc-mod and intero support calling out to djinn (I can't test this, as I can't get either to work on NixOS :( ).
For a little more work, you could write properties for QuickCheck (/SmallCheck/LazySmallCheck/etc.) to constrain the behaviour, which would allow trivial solutions like the empty list to be ruled out automatically. If you're a TDD disciple, then you already wrote these properties, so this part would actually be free (as long as the automation tooling exists).
At that point you're basically doing inductive functional programming, so tools like IGOR2 or MagicHaskeller might be useful to plug in as well.
As mentioned below, this can be used in languages like Agda and Idris; they also give you proof search, which tries to automatically fill in the holes from available definitions. This works well for 'proof objects' (the name given to values which only exist to satisfy the type checker), but requires caution for values with 'computational content' (those values which can effect the resulting computation).
Pretty much all Haskell code (except the really wacky astronautical stuff) has computational content, so there are fewer "obvious" obligations to fill in than would appear in a proof (in fact, due to laziness and lack of totality, we can safely use 'undefined' for all proof objects, since they'll never be pattern-matched!).
For example, if our function needs to return a list (e.g. if we're writing a function like map, filter, iterate, replicate, cycle, etc.), a proof search will immediately give us the empty list '[]', which is correctly typed but probably wrong.
For Haskell, tools like djinn can get you a little hole-filling automation, and I think that Emacs modes like ghc-mod and intero support calling out to djinn (I can't test this, as I can't get either to work on NixOS :( ).
For a little more work, you could write properties for QuickCheck (/SmallCheck/LazySmallCheck/etc.) to constrain the behaviour, which would allow trivial solutions like the empty list to be ruled out automatically. If you're a TDD disciple, then you already wrote these properties, so this part would actually be free (as long as the automation tooling exists).
At that point you're basically doing inductive functional programming, so tools like IGOR2 or MagicHaskeller might be useful to plug in as well.