> If you return the same proof of correctness that you used > for the earlier definition of sort, then no it won't type check. > But if you return a proof defined as e.g. > > proof = proof > > then if I understand things correctly it will type check. On that note, since this has been of interest on comp.lang.functional: Howabout a way to tell the compiler: "don't allow general recursion"?
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Martin Norb{ck
- Re: Haskell 2 -- Dependent types? Olivier . Lefevre
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- RE: Haskell 2 -- Dependent types? Nick Kallen
- RE: Haskell 2 -- Dependent types? Nick Kallen
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Lennart Augustsson
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- RE: Haskell 2 -- Dependent types? Nick Kallen
- Re: Haskell 2 -- Dependent types? Fergus Henderson
- Re: Haskell 2 -- Dependent types? Carl R. Witty