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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users