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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Bas van Dijk-2
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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Alexander Vershilov
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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



--
Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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 <[hidden email]> 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 <[hidden email]> 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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> --
> Alexander
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Alexander 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>>
>> --
>> Alexander
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>



--
Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Bas van Dijk-2
Hi Alexander,

Thanks for your answer! This provides a lot of ideas how to proceed.

I'm unsure about the following though:

> 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

Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
not just the Nat inside the SomeNat?

I also see that p is only used for comparing it to k. It's not used to
produce the return value.

Cheers,

Bas

On 25 November 2014 at 19:55, Alexander V Vershilov
<[hidden email]> wrote:

> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>>> [hidden email]
>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>>
>>>
>>> --
>>> Alexander
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>
>
>
>
> --
> Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Bas van Dijk-2
In reply to this post by Richard Eisenberg-2
On 25 November 2014 at 19:34, Richard Eisenberg <[hidden email]> wrote:
> 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.

Thanks, I hadn't considered this yet.

Cheers,

Bas
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Alexander Vershilov
In reply to this post by Bas van Dijk-2
Hi, Bas, Richard.

I've played a bit with example, obvously first approach contained bugs,
but seems that I have fixed it and here I have 2 approaches, one uses
unsafeCoerce (as Richard suggested) another is safe but with bad complexity:

Full file is quite big, so I'm not inlining it in mail, but here is a link:

https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs

I wonder how far it's possible to go with singletons approach that I have
not tried yet.

--
Alexander

On 26 November 2014 at 10:15, Bas van Dijk <[hidden email]> wrote:

> Hi Alexander,
>
> Thanks for your answer! This provides a lot of ideas how to proceed.
>
> I'm unsure about the following though:
>
>> 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
>
> Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
> not just the Nat inside the SomeNat?
>
> I also see that p is only used for comparing it to k. It's not used to
> produce the return value.
>
> Cheers,
>
> Bas
>
> On 25 November 2014 at 19:55, Alexander V Vershilov
> <[hidden email]> wrote:
>> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>>>> [hidden email]
>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>
>>>>
>>>>
>>>> --
>>>> Alexander
>>>> _______________________________________________
>>>> Glasgow-haskell-users mailing list
>>>> [hidden email]
>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>
>>>
>>
>>
>>
>> --
>> Alexander



--
Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
Hi Alexander,

Nice idea to test against the set of known values. That's more type-safe than anything I've thought of. I agree that it's a bit of a painful construction, but I don't think we can do better with type-lits, as there is limited reasoning ability that GHC can manage. If you want to switch to unary naturals (`data Nat = Zero | Succ Nat`), then this can be built somewhat nicely with singletons and without unsafeCoerce. But, of course, unary naturals are very slow.

By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3 -- not in .2 or in the soon-to-be .4) that allows you to write unsaturated type families that don't work. Saying `LessThan255` without a parameter should be a syntax error, but that check was accidentally turned off for 7.8.3, leading to a bogus type error.

Thanks for sharing this work!
Richard

On Nov 28, 2014, at 5:27 PM, Alexander V Vershilov <[hidden email]> wrote:

> Hi, Bas, Richard.
>
> I've played a bit with example, obvously first approach contained bugs,
> but seems that I have fixed it and here I have 2 approaches, one uses
> unsafeCoerce (as Richard suggested) another is safe but with bad complexity:
>
> Full file is quite big, so I'm not inlining it in mail, but here is a link:
>
> https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs
>
> I wonder how far it's possible to go with singletons approach that I have
> not tried yet.
>
> --
> Alexander
>
> On 26 November 2014 at 10:15, Bas van Dijk <[hidden email]> wrote:
>> Hi Alexander,
>>
>> Thanks for your answer! This provides a lot of ideas how to proceed.
>>
>> I'm unsure about the following though:
>>
>>> 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
>>
>> Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
>> not just the Nat inside the SomeNat?
>>
>> I also see that p is only used for comparing it to k. It's not used to
>> produce the return value.
>>
>> Cheers,
>>
>> Bas
>>
>> On 25 November 2014 at 19:55, Alexander V Vershilov
>> <[hidden email]> wrote:
>>> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>>>>> [hidden email]
>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>
>>>>>
>>>>>
>>>>> --
>>>>> Alexander
>>>>> _______________________________________________
>>>>> Glasgow-haskell-users mailing list
>>>>> [hidden email]
>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>
>>>>
>>>
>>>
>>>
>>> --
>>> Alexander
>
>
>
> --
> Alexander
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Alexander Vershilov
Hi, Richard

Can you give some ideas or where to read how to properly use signletons
and unary naturals in order to be able to express such constraints?

Thanks
--
  Alexander

On 30 November 2014 at 23:26, Richard Eisenberg <[hidden email]> wrote:

> Hi Alexander,
>
> Nice idea to test against the set of known values. That's more type-safe than anything I've thought of. I agree that it's a bit of a painful construction, but I don't think we can do better with type-lits, as there is limited reasoning ability that GHC can manage. If you want to switch to unary naturals (`data Nat = Zero | Succ Nat`), then this can be built somewhat nicely with singletons and without unsafeCoerce. But, of course, unary naturals are very slow.
>
> By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3 -- not in .2 or in the soon-to-be .4) that allows you to write unsaturated type families that don't work. Saying `LessThan255` without a parameter should be a syntax error, but that check was accidentally turned off for 7.8.3, leading to a bogus type error.
>
> Thanks for sharing this work!
> Richard
>
> On Nov 28, 2014, at 5:27 PM, Alexander V Vershilov <[hidden email]> wrote:
>
>> Hi, Bas, Richard.
>>
>> I've played a bit with example, obvously first approach contained bugs,
>> but seems that I have fixed it and here I have 2 approaches, one uses
>> unsafeCoerce (as Richard suggested) another is safe but with bad complexity:
>>
>> Full file is quite big, so I'm not inlining it in mail, but here is a link:
>>
>> https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs
>>
>> I wonder how far it's possible to go with singletons approach that I have
>> not tried yet.
>>
>> --
>> Alexander
>>
>> On 26 November 2014 at 10:15, Bas van Dijk <[hidden email]> wrote:
>>> Hi Alexander,
>>>
>>> Thanks for your answer! This provides a lot of ideas how to proceed.
>>>
>>> I'm unsure about the following though:
>>>
>>>> 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
>>>
>>> Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
>>> not just the Nat inside the SomeNat?
>>>
>>> I also see that p is only used for comparing it to k. It's not used to
>>> produce the return value.
>>>
>>> Cheers,
>>>
>>> Bas
>>>
>>> On 25 November 2014 at 19:55, Alexander V Vershilov
>>> <[hidden email]> wrote:
>>>> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>>>>>> [hidden email]
>>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>>
>>>>>>
>>>>>>
>>>>>> --
>>>>>> Alexander
>>>>>> _______________________________________________
>>>>>> Glasgow-haskell-users mailing list
>>>>>> [hidden email]
>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>>
>>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> Alexander
>>
>>
>>
>> --
>> Alexander
>>
>



--
Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
Sadly, I don't have a go-to place for this stuff. Perhaps it will be helpful to see an example of this in action? Here is my unary version of this:

> {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, TypeFamilies,
>              ScopedTypeVariables, TypeOperators, UndecidableInstances,
>              GADTs, RankNTypes #-}
> {-# OPTIONS_GHC -ftype-function-depth=300 -fcontext-stack=300 #-}
>
> import Data.Singletons.TH
> import GHC.TypeLits hiding ( Nat )
>
> $(singletons [d|
>   data Nat = Zero | Succ Nat
>
>   leNat :: Nat -> Nat -> Bool
>   leNat Zero     _        = True
>   leNat (Succ _) Zero     = False
>   leNat (Succ a) (Succ b) = a `leNat` b
>   |])
>
> -- | Singletons's 'withSomeSing' is what we want, but a bug in 7.8.3 doesn't
> -- let it work without a specialized type for 'Nat's
> withSomeNat :: Nat -> (forall (n :: Nat). Sing n -> r) -> r
> withSomeNat = withSomeSing
>
> -- | Conveniently generate unary naturals
> type family U n where
>   U 0 = Zero
>   U n = Succ (U (n-1))
>
> toNat :: Integer -> Maybe Nat
> toNat n | n < 0      = Nothing
>         | otherwise  = Just $ go n
>   where
>     go 0 = Zero
>     go n = Succ (go (n-1))
>
> type Bound = U 255
>
> -- easier to test in GHCi than a proper 'main'
> go :: Integer -> IO ()
> go n =
>    case toNat n of
>      Nothing  -> putStrLn "Input is not a natural number!"
>      Just nat -> putStrLn $ withSomeNat nat $ \ snat ->
>        case snat `sLeNat` (sing :: Sing Bound) of
>          STrue  -> f snat
>          SFalse -> "Didn't work"
>
> f :: forall proxy (n :: Nat). (n `LeNat` Bound) ~ True => proxy n -> String
> f _ = "It worked!"

I'm happy to answer questions, but it's hard to know how much detail to use in a description of the code.

I hope this helps,
Richard

On Dec 4, 2014, at 5:50 PM, Alexander V Vershilov <[hidden email]> wrote:

> Hi, Richard
>
> Can you give some ideas or where to read how to properly use signletons
> and unary naturals in order to be able to express such constraints?
>
> Thanks
> --
>  Alexander
>
> On 30 November 2014 at 23:26, Richard Eisenberg <[hidden email]> wrote:
>> Hi Alexander,
>>
>> Nice idea to test against the set of known values. That's more type-safe than anything I've thought of. I agree that it's a bit of a painful construction, but I don't think we can do better with type-lits, as there is limited reasoning ability that GHC can manage. If you want to switch to unary naturals (`data Nat = Zero | Succ Nat`), then this can be built somewhat nicely with singletons and without unsafeCoerce. But, of course, unary naturals are very slow.
>>
>> By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3 -- not in .2 or in the soon-to-be .4) that allows you to write unsaturated type families that don't work. Saying `LessThan255` without a parameter should be a syntax error, but that check was accidentally turned off for 7.8.3, leading to a bogus type error.
>>
>> Thanks for sharing this work!
>> Richard
>>
>> On Nov 28, 2014, at 5:27 PM, Alexander V Vershilov <[hidden email]> wrote:
>>
>>> Hi, Bas, Richard.
>>>
>>> I've played a bit with example, obvously first approach contained bugs,
>>> but seems that I have fixed it and here I have 2 approaches, one uses
>>> unsafeCoerce (as Richard suggested) another is safe but with bad complexity:
>>>
>>> Full file is quite big, so I'm not inlining it in mail, but here is a link:
>>>
>>> https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs
>>>
>>> I wonder how far it's possible to go with singletons approach that I have
>>> not tried yet.
>>>
>>> --
>>> Alexander
>>>
>>> On 26 November 2014 at 10:15, Bas van Dijk <[hidden email]> wrote:
>>>> Hi Alexander,
>>>>
>>>> Thanks for your answer! This provides a lot of ideas how to proceed.
>>>>
>>>> I'm unsure about the following though:
>>>>
>>>>> 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
>>>>
>>>> Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
>>>> not just the Nat inside the SomeNat?
>>>>
>>>> I also see that p is only used for comparing it to k. It's not used to
>>>> produce the return value.
>>>>
>>>> Cheers,
>>>>
>>>> Bas
>>>>
>>>> On 25 November 2014 at 19:55, Alexander V Vershilov
>>>> <[hidden email]> wrote:
>>>>> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
>>>>>>>> [hidden email]
>>>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> --
>>>>>>> Alexander
>>>>>>> _______________________________________________
>>>>>>> Glasgow-haskell-users mailing list
>>>>>>> [hidden email]
>>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>> --
>>>>> Alexander
>>>
>>>
>>>
>>> --
>>> Alexander
>>>
>>
>
>
>
> --
> Alexander
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Ranjit Jhala
Dear Alexander, 

FWIW, this sort of thing is quite straightforward with LiquidHaskell:


or, the code below:

-----

{-@ LIQUID "--no-termination" @-}

module Nat255 where

-- | Define a predicate for valid integers

{-@ predicate IsValid X = 0 <= X && X < 255 @-}

-- | Use the predicate to define a refinement type (subset) of valid integers

{-@ type Valid = {v:Int | IsValid v}        @-}

-- | A function that checks whether a given Int is indeed valid

{-@ isValid   :: n:Int -> {v:Bool | Prop v <=> IsValid n} @-}
isValid n     = 0 <= n && n < (255 :: Int)

-- | A function that can only be called with Valid Ints.

{-@ workWithValidNumber :: Valid -> IO () @-} 
workWithValidNumber n = putStrLn $ "This is a valid number" ++ show (n :: Int)

-- | This is fine...
ok    = workWithValidNumber 12

-- | ... But this is not.        
notOk = workWithValidNumber 257

-- | Finally the top level loop that inputs a number, tests it 
--   and calls `workWithValidNumber` if the number is valid.

loop = do putStrLn "Enter Number between 0 and 255"
          n <- readLn :: IO Int
          if isValid n
             then workWithValidNumber n
             else putStrLn "Humph, bad input, try again!" >> loop


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

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

Alexander Vershilov
Richard, Ranjit,

Thanks for providing your solutions.

--
Alexander.

On 8 December 2014 at 21:45, Ranjit Jhala <[hidden email]> wrote:

> Dear Alexander,
>
> FWIW, this sort of thing is quite straightforward with LiquidHaskell:
>
> http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1418064183.hs
>
> or, the code below:
>
> -----
>
> {-@ LIQUID "--no-termination" @-}
>
> module Nat255 where
>
> -- | Define a predicate for valid integers
>
> {-@ predicate IsValid X = 0 <= X && X < 255 @-}
>
> -- | Use the predicate to define a refinement type (subset) of valid
> integers
>
> {-@ type Valid = {v:Int | IsValid v}        @-}
>
> -- | A function that checks whether a given Int is indeed valid
>
> {-@ isValid   :: n:Int -> {v:Bool | Prop v <=> IsValid n} @-}
> isValid n     = 0 <= n && n < (255 :: Int)
>
> -- | A function that can only be called with Valid Ints.
>
> {-@ workWithValidNumber :: Valid -> IO () @-}
> workWithValidNumber n = putStrLn $ "This is a valid number" ++ show (n ::
> Int)
>
> -- | This is fine...
> ok    = workWithValidNumber 12
>
> -- | ... But this is not.
> notOk = workWithValidNumber 257
>
> -- | Finally the top level loop that inputs a number, tests it
> --   and calls `workWithValidNumber` if the number is valid.
>
> loop = do putStrLn "Enter Number between 0 and 255"
>           n <- readLn :: IO Int
>           if isValid n
>              then workWithValidNumber n
>              else putStrLn "Humph, bad input, try again!" >> loop
>



--
Alexander
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users