positive type-level naturals

[Carter Schonwald]

its a special Thing that just uses Integer internally, but because it
doenst provide a PEANO api, we can't do computations on it :'(




On Sun, Mar 16, 2014 at 10:37 AM, Henning Thielemann <
lemming at henning-thielemann.de> wrote:

> Am 16.03.2014 14:35, schrieb Carter Schonwald:
>
>
>  You can't with type lits. The solver can only decide concrete values :"""(
>>
>
> I hoped that with type-level natural numbers all my dreams would become
> true. :-)
>
> I'd be also happy if I could manually provide the proof for 1<=n+1 and
> more complicated statements like n+n=2*n and n>0 && m>0 => n*m>0.
>
>
>  You'll have to use a concrete peano Nats type instead.
>>
>
> That is, I may as well stay with the existing type-level number packages?
>
>
>  I've been toying with the idea that the type lits syntax should be just
>> that, a type level analogue of from integer that you can give to user
>> land types, but I'm not going to suggest that till 7.8 is fully released.
>>
>
> Seems reasonable. By the way, is the GHC Nat kind defined by data
> promotion or is it a special kind with an efficient internal representation?
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140316/baa89ee6/attachment.html>