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

12 messages
Open this post in threaded view
|

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

 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 :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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|

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

 In reply to this post by Richard Eisenberg-2 On 25 November 2014 at 19:34, Richard Eisenberg <[hidden email]> wrote: > If I were you, I would just write `g` using unsafeCoerce in the right spot, instead of bothering with all the singletons, which would have to use unsafety anyway. Thanks, I hadn't considered this yet. Cheers, Bas _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|