Hi, Bas, Richard. I've played a bit with example, obvously first approach contained bugs, but seems that I have fixed it and here I have 2 approaches, one uses unsafeCoerce (as Richard suggested) another is safe but with bad complexity:
Full file is quite big, so I'm not inlining it in mail, but here is a link: https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs I wonder how far it's possible to go with singletons approach that I have not tried yet. -- Alexander On 26 November 2014 at 10:15, Bas van Dijk <v.dijk....@gmail.com> wrote: > Hi Alexander, > > Thanks for your answer! This provides a lot of ideas how to proceed. > > I'm unsure about the following though: > >> lessThen :: KnownNat m => SomeNat -> Proxy m -> Maybe (Proof (n <= m) (Proxy >> n)) >> lessThen (SomeNat p) k >> | natVal p <= natVal k = Just (Proof $ Tagged (Proxy :: Proxy n)) >> | otherwise = Nothing > > Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and > not just the Nat inside the SomeNat? > > I also see that p is only used for comparing it to k. It's not used to > produce the return value. > > Cheers, > > Bas > > On 25 November 2014 at 19:55, Alexander V Vershilov > <alexander.vershi...@gmail.com> wrote: >> Hi, Richard, Bas. >> >> Maybe I didn't spell it properly but my point was to create a data >> type that carry a proof >> without exposing it's constructor and having clever constructor only, >> then the only place >> where you need to check will be that constructor. >> >> Also it's possible to write in slightly clearer, but again it's >> possible to make a mistake here >> and it will be a false proof. >> >>> lessThen :: KnownNat m => SomeNat -> Proxy m -> Maybe (Proof (n <= m) >>> (Proxy n)) >>> lessThen (SomeNat p) k >>> | natVal p <= natVal k = Just (Proof $ Tagged (Proxy :: Proxy n)) >>> | otherwise = Nothing >> >> Of cause solution using singletons could solve this problem much better. >> >> -- >> Alexander >> >> On 25 November 2014 at 21:34, Richard Eisenberg <e...@cis.upenn.edu> wrote: >>> Hi Bas, >>> >>> I believe to do this "right", you would need singleton types. Then, when >>> you discover that the number is bounded by 255, you would also discover >>> that the type is bounded by 255, and you'd be home free. >>> >>> Unfortunately, I there isn't currently a way to do comparison on >>> GHC.TypeLits Nats with singletons. (There is a module >>> Data.Singletons.TypeLits in the `singletons` package, but there's a comment >>> telling me TODO in the part where comparison should be implemented.) If it >>> were implemented, it would have to use unsafeCoerce, as there's no built-in >>> mechanism connecting runtime numbers with TypeLits. >>> >>> 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. >>> >>> The solution Alexander provides below doesn't quite build a proof, I think. >>> Tellingly, if we omit the `natVal p <= 255` check, everything else still >>> compiles. Thus, the `Proof` type he uses can be built even if the fact >>> proven is false. That said, I don't know if my solution is any better, >>> crucially relying on unsafeCoerce. >>> >>> Richard >>> >>> On Nov 25, 2014, at 4:52 AM, Alexander V Vershilov >>> <alexander.vershi...@gmail.com> wrote: >>> >>>> 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....@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@haskell.org >>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>>> >>>> >>>> >>>> -- >>>> Alexander >>>> _______________________________________________ >>>> Glasgow-haskell-users mailing list >>>> Glasgow-haskell-users@haskell.org >>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>>> >>> >> >> >> >> -- >> Alexander -- Alexander _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
