positive type-level naturals

[Carter Schonwald]

respectfully,
The current typeLits story for nats is kinda a fuster cluck to put it
politely . We have type lits but we cant use them (well, we can't compute
on them, which is the same thing).

For the past 2 years, every ghc release cycle, I first discover, then have
to communicate to everyone else "you can't compute on type lits".

Heres what I'd like to happen for 7.10, and i'm happy to help / pester this
along

1) Typelits as it currently exists in GHC actually conflates "syntactic
support" for Nats with having primacy as the "nat" type for ghc.
I think we should seriously consider moving in a direction akin to how Agda
provides syntactic/ computational support for efficient /

2) the current typelits supplied Nat is kinda crippled because we can't do
userland reasoning / compute on it, I consider this a bug! I'm still
waiting (2 years later) for a solver we can actually include in ghc or even
a user land solver!

i think (1) and some part of (2) should happen for 7.10. What design work /
subtleties might block it?



On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij <
christiaan.baaij at gmail.com> wrote:

> Iavor is working on a branch that allows the constraint solver to call an
> external solver: https://github.com/ghc/ghc/tree/decision-procedure
> Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly
> out of of line with HEAD.
> I think the above branch will be able to solve things like: 1 <= n + 1 ~
> True
>
> I myself worked on a patch that can only work with equalities:
> https://gist.github.com/christiaanb/8396614
> It allows you to solve both more and less constraints than Iavor's CVC4
> approach:
> More: It can deal with non-constant multiplications, and also with
> exponentials
> Less: It cannot deal with inequalities
>
>
>
> On Sun, Mar 16, 2014 at 1:44 PM, Henning Thielemann <
> lemming at henning-thielemann.de> wrote:
>
>> Am 16.03.2014 09:40, schrieb Christiaan Baaij:
>>
>>  To answer the second question (under the assumption that you want
>>> phantom-type style Vectors and not GADT-style):
>>>
>>
>> Now I like to define non-empty vectors. The phantom parameter for the
>> length shall refer to the actual vector length, not to length-1, for
>> consistency between possibly empty and non-empty vectors.
>>
>> I have modified your code as follows:
>>
>> {-# LANGUAGE Rank2Types #-}
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE KindSignatures #-}
>> {-# LANGUAGE ScopedTypeVariables #-}
>> {-# LANGUAGE TypeOperators #-}
>> {-# LANGUAGE TypeFamilies #-}
>> module PositiveNat where
>>
>> import Data.Proxy (Proxy(Proxy))
>> import GHC.TypeLits
>>           (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal,
>>            type (<=), type (+))
>>
>> data Vector (n :: Nat) a = Vector a [a]
>>
>> withVector ::
>>    forall a b.
>>    a -> [a] ->
>>    (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b
>> withVector x xs f =
>>    case someNatVal $ toInteger $ length xs of
>>       Nothing -> error "static/dynamic mismatch"
>>       Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)
>>
>> vecLen :: forall n . KnownNat n => Vector n Integer -> Integer
>> vecLen _ = natVal (Proxy :: Proxy n)
>>
>> -- > withVector vecLen [1,2,3,4]
>> -- 4
>>
>>
>> GHC-7.8 complains with:
>>
>> PositiveNat.hs:23:40:
>>     Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True)
>>     from the context (KnownNat n)
>>       bound by a pattern with constructor
>>                  SomeNat :: forall (n :: Nat). KnownNat n => Proxy n ->
>> SomeNat,
>>                in a case alternative
>>       at PositiveNat.hs:23:13-34
>>     In the expression: f (Vector x xs :: Vector (m + 1) a)
>>     In a case alternative:
>>         Just (SomeNat (_ :: Proxy m))
>>           -> f (Vector x xs :: Vector (m + 1) a)
>>     In the expression:
>>       case someNatVal $ toInteger $ length xs of {
>>         Nothing -> error "static/dynamic mismatch"
>>         Just (SomeNat (_ :: Proxy m))
>>           -> f (Vector x xs :: Vector (m + 1) a) }
>>
>>
>> How can I convince GHC that n+1 is always at least 1?
>>
>>
>> When I remove the (1<=n) constraint, I still get:
>>
>> PositiveNat.hs:23:40:
>>     Could not deduce (KnownNat (n + 1)) arising from a use of ‘f’
>>     from the context (KnownNat n)
>>       bound by a pattern with constructor
>>                  SomeNat :: forall (n :: Nat). KnownNat n => Proxy n ->
>> SomeNat,
>>                in a case alternative
>>       at PositiveNat.hs:23:13-34
>>     In the expression: f (Vector x xs :: Vector (m + 1) a)
>>     In a case alternative:
>>         Just (SomeNat (_ :: Proxy m))
>>           -> f (Vector x xs :: Vector (m + 1) a)
>>     In the expression:
>>       case someNatVal (toInteger (length xs)) of {
>>         Nothing -> error "static/dynamic mismatch"
>>         Just (SomeNat (_ :: Proxy m))
>>           -> f (Vector x xs :: Vector (m + 1) a) }
>>
>> That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is
>> also KnownNat. How to do that?
>>
>>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140316/34eff6c3/attachment.html>