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

25 Nov 2014


      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

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

Alexander V Vershilov