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

[Alexander V 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 <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