Hi, Richard Can you give some ideas or where to read how to properly use signletons and unary naturals in order to be able to express such constraints?
Thanks -- Alexander On 30 November 2014 at 23:26, Richard Eisenberg <[email protected]> wrote: > 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 > <[email protected]> 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 <[email protected]> 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 >>> <[email protected]> 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 <[email protected]> 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 >>>>> <[email protected]> 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 <[email protected]> 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 >>>>>>> [email protected] >>>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>>>>> >>>>>> >>>>>> >>>>>> -- >>>>>> Alexander >>>>>> _______________________________________________ >>>>>> Glasgow-haskell-users mailing list >>>>>> [email protected] >>>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>>>>> >>>>> >>>> >>>> >>>> >>>> -- >>>> Alexander >> >> >> >> -- >> Alexander >> > -- Alexander _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
