... | @@ -36,7 +36,7 @@ As can be seen here, goals are numbered, and the typechecker returns the inferre |
... | @@ -36,7 +36,7 @@ As can be seen here, goals are numbered, and the typechecker returns the inferre |
|
|
|
|
|
These goals can make it a lot easier to write code. They allow typechecking to continue although certain parts of code are missing and they work as a TODO list.
|
|
These goals can make it a lot easier to write code. They allow typechecking to continue although certain parts of code are missing and they work as a TODO list.
|
|
|
|
|
|
# How this can be used in GHC now
|
|
# How we can almost do this in GHC now
|
|
|
|
|
|
|
|
|
|
GHC does not support holes in the way Agda does. It is possible to insert `undefined` in an expression to make it typecheck (which Agda doesn't have), but this is not very helpful when writing software. Inserting `undefined` only gives as information that the rest of the program typechecks, but will not help you find what you needed to use in its place. We propose to add an extension to GHC (and notably GHCi) to allow using holes, this page is meant to discuss the exact features and workflow of such an extension.
|
|
GHC does not support holes in the way Agda does. It is possible to insert `undefined` in an expression to make it typecheck (which Agda doesn't have), but this is not very helpful when writing software. Inserting `undefined` only gives as information that the rest of the program typechecks, but will not help you find what you needed to use in its place. We propose to add an extension to GHC (and notably GHCi) to allow using holes, this page is meant to discuss the exact features and workflow of such an extension.
|
... | | ... | |