Hello, I've added a section with my notes on the minimal semantics required to address what Haskell lacks with respect to strict types. Ed Kmett pointed me to some stuff that I think may fix all the problems with the !T sort of solution. It builds on the new constraint being considered for handling impredicativity. The quick sketch goes like this. Given the declaration: data Nat = Z | S !Nat then: Nat :: * !Nat :: Unlifted S :: Nat -> Nat But we also have: !Nat <~ Nat and the witness of this is just an identity function, because all values of type !Nat are legitimate values of type Nat. Then we can have: case n of S m -> ... Z -> ... where m has type !Nat, but we can still call `S m` and the like, because !Nat <~ Nat. If we do use `S m`, the S call will do some unnecessary evaluation of m, but this can (hopefully) be fixed with an optimization based on knowing that m has type !Nat, which we are weakening to Nat. Thoughts? -- Dan On Thu, Oct 8, 2015 at 8:36 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
On Oct 8, 2015, at 6:02 AM, Simon Peyton Jones <simonpj@microsoft.com> wrote:
What's the wiki page?