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

26 Nov 2014

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