Proving properties of type-level natural numbers obtained from user input
Alexander V Vershilov
alexander.vershilov at gmail.com
Tue Nov 25 09:52:12 UTC 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 <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
More information about the Glasgow-haskell-users
mailing list