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