Proving properties of type-level natural numbers obtained from user input
Bas van Dijk
v.dijk.bas at gmail.com
Tue Nov 25 07:51:11 UTC 2014
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
More information about the Glasgow-haskell-users
mailing list