Proving properties of type-level natural numbers obtained from user input

[Alexander V Vershilov]

Hi, Richard, Bas.

Maybe I didn't spell it properly but my point was to create a data
type that carry a proof
without exposing it's constructor and having clever constructor only,
then the only place
where you need to check will be that constructor.

Also it's possible to write in slightly clearer, but again it's
possible to make a mistake here
and it will be a false proof.

> lessThen :: KnownNat m => SomeNat -> Proxy m -> Maybe (Proof (n <= m) (Proxy n))
> lessThen (SomeNat p) k
>    | natVal p <= natVal k = Just (Proof $ Tagged (Proxy :: Proxy n))
>    | otherwise = Nothing

Of cause solution using singletons could solve this problem much better.

--
Alexander

On 25 November 2014 at 21:34, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> Hi Bas,
>
> I believe to do this "right", you would need singleton types. Then, when you discover that the number is bounded by 255, you would also discover that the type is bounded by 255, and you'd be home free.
>
> Unfortunately, I there isn't currently a way to do comparison on GHC.TypeLits Nats with singletons. (There is a module Data.Singletons.TypeLits in the `singletons` package, but there's a comment telling me TODO in the part where comparison should be implemented.) If it were implemented, it would have to use unsafeCoerce, as there's no built-in mechanism connecting runtime numbers with TypeLits.
>
> If I were you, I would just write `g` using unsafeCoerce in the right spot, instead of bothering with all the singletons, which would have to use unsafety anyway.
>
> The solution Alexander provides below doesn't quite build a proof, I think. Tellingly, if we omit the `natVal p <= 255` check, everything else still compiles. Thus, the `Proof` type he uses can be built even if the fact proven is false. That said, I don't know if my solution is any better, crucially relying on unsafeCoerce.
>
> Richard
>
> On Nov 25, 2014, at 4:52 AM, Alexander V Vershilov <alexander.vershilov at gmail.com> wrote:
>
>> Hi,
>>
>> Following approach can work, the idea is to define a type that will
>> carry a proof (constraint) that we want to check. Here I have reused
>> Data.Tagged, but it's possible to introduce your own with concrete
>> constraints.
>>
>>> {-# LANGUAGE DataKinds #-}
>>> {-# LANGUAGE GADTs #-}
>>> {-# LANGUAGE TypeOperators #-}
>>> {-# LANGUAGE KindSignatures #-}
>>> {-# LANGUAGE PolyKinds #-}
>>> {-# LANGUAGE UndecidableInstances #-}
>>> import GHC.TypeLits
>>> import GHC.Exts
>>> import Data.Proxy
>>> import Data.Tagged
>>> import System.Environment
>>
>> New constraint carrying data type
>>
>>> newtype Proof a b = Proof { unProof :: Tagged a b }
>>
>> Runtime check for unknown naturals
>>
>>> fromSome :: SomeNat -> Maybe (Proof (n <= 255) (Proxy n))
>>> fromSome (SomeNat p)
>>>   | natVal p <= 255 = Just (Proof $ Tagged (Proxy :: Proxy n))
>>>   | otherwise = Nothing
>>
>> Compiletime converter for known naturals
>>
>>> fromKnown :: (KnownNat n,  n <= 255) => Proxy n -> Proof (n <= 255) (Proxy n)
>>> fromKnown n = Proof $ Tagged n
>>
>> Function to test:
>>
>>> f2 :: (c ~ (n <= 255)) => Proof c (Proxy n) -> ()
>>> f2 _ = ()
>>
>> Example of use:
>>
>>> main :: IO ()
>>> main = do
>>>    [arg] <- getArgs
>>>    let n = read arg :: Integer
>>>
>>>    case someNatVal n of
>>>      Nothing -> error "Input is not a natural number!"
>>>      Just sn -> case fromSome sn of
>>>                   Just p -> return $ f2 p
>>>                   _ -> error "Input if larger than 255"
>>
>>
>> On 25 November 2014 at 10:51, Bas van Dijk <v.dijk.bas at gmail.com> wrote:
>>> Hi,
>>>
>>> I have another type-level programming related question:
>>>
>>>> {-# LANGUAGE GADTs #-}
>>>> {-# LANGUAGE TypeOperators #-}
>>>> {-# LANGUAGE ScopedTypeVariables #-}
>>>> {-# LANGUAGE KindSignatures #-}
>>>>
>>>> import GHC.TypeLits
>>>
>>> Say I have a Proxy p of some type-level natural number:
>>>
>>>> p :: forall (n :: Nat). Proxy n
>>>> p = Proxy
>>>
>>> Imagine I get p from user input like this:
>>>
>>>> main :: IO ()
>>>> main = do
>>>>    [arg] <- getArgs
>>>>    let n = read arg :: Integer
>>>>
>>>>    case someNatVal n of
>>>>      Nothing -> error "Input is not a natural number!"
>>>>      Just (SomeNat (p :: Proxy n)) -> ...
>>>
>>> I also have a function f which takes a proxy of a natural number but
>>> it has the additional constraint that the number should be lesser than
>>> or equal to 255:
>>>
>>>> f :: forall (n :: Nat). (n <= 255) => proxy n -> ()
>>>> f _ = ()
>>>
>>> How do I apply f to p?
>>>
>>> Obviously, applying it directly gives the type error:
>>>
>>>> f p
>>> <interactive>:179:1:
>>>    Couldn't match expected type ‘'True’ with actual type ‘n0 <=? 255’
>>>    The type variable ‘n0’ is ambiguous
>>>    In the expression: f p
>>>    In an equation for ‘it’: it = f p
>>>
>>> I imagine I somehow need to construct some Proof object using a function g like:
>>>
>>>> g :: forall (n :: Nat). proxy n -> Proof
>>>> g _ = ...
>>>
>>> Where the Proof constructor encapsulates the (n <= 255) constraint:
>>>
>>>> data Proof where
>>>>    NoProof :: Proof
>>>>    Proof :: forall (n :: Nat). (n <= 255)
>>>>          => Proxy n -> Proof
>>>
>>> With g in hand I can construct c which patterns matches on g p and
>>> when there's a Proof the (n <= 255) constraint will be in scope which
>>> allows applying f to p:
>>>
>>>> c :: ()
>>>> c = case g p of
>>>>      NoProof -> error "Input is bigger than 255!"
>>>>      Proof p -> f p
>>>
>>> But how do I define g?
>>>
>>> Cheers,
>>>
>>> Bas
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users at haskell.org
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>>
>> --
>> Alexander
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>



-- 
Alexander