Hi Alexander, Nice idea to test against the set of known values. That's more type-safe than anything I've thought of. I agree that it's a bit of a painful construction, but I don't think we can do better with type-lits, as there is limited reasoning ability that GHC can manage. If you want to switch to unary naturals (`data Nat = Zero | Succ Nat`), then this can be built somewhat nicely with singletons and without unsafeCoerce. But, of course, unary naturals are very slow.
By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3 -- not in .2 or in the soon-to-be .4) that allows you to write unsaturated type families that don't work. Saying `LessThan255` without a parameter should be a syntax error, but that check was accidentally turned off for 7.8.3, leading to a bogus type error. Thanks for sharing this work! Richard On Nov 28, 2014, at 5:27 PM, Alexander V Vershilov <alexander.vershi...@gmail.com> wrote: > 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
