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

25 Nov 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

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

Bas van Dijk