Sadly, I don't have a go-to place for this stuff. Perhaps it will be helpful to
see an example of this in action? Here is my unary version of this:
> {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, TypeFamilies,
> ScopedTypeVariables, TypeOperators, UndecidableInstances,
> GADTs, RankNTypes #-}
> {-# OPTIONS_GHC -ftype-function-depth=300 -fcontext-stack=300 #-}
>
> import Data.Singletons.TH
> import GHC.TypeLits hiding ( Nat )
>
> $(singletons [d|
> data Nat = Zero | Succ Nat
>
> leNat :: Nat -> Nat -> Bool
> leNat Zero _ = True
> leNat (Succ _) Zero = False
> leNat (Succ a) (Succ b) = a `leNat` b
> |])
>
> -- | Singletons's 'withSomeSing' is what we want, but a bug in 7.8.3 doesn't
> -- let it work without a specialized type for 'Nat's
> withSomeNat :: Nat -> (forall (n :: Nat). Sing n -> r) -> r
> withSomeNat = withSomeSing
>
> -- | Conveniently generate unary naturals
> type family U n where
> U 0 = Zero
> U n = Succ (U (n-1))
>
> toNat :: Integer -> Maybe Nat
> toNat n | n < 0 = Nothing
> | otherwise = Just $ go n
> where
> go 0 = Zero
> go n = Succ (go (n-1))
>
> type Bound = U 255
>
> -- easier to test in GHCi than a proper 'main'
> go :: Integer -> IO ()
> go n =
> case toNat n of
> Nothing -> putStrLn "Input is not a natural number!"
> Just nat -> putStrLn $ withSomeNat nat $ \ snat ->
> case snat `sLeNat` (sing :: Sing Bound) of
> STrue -> f snat
> SFalse -> "Didn't work"
>
> f :: forall proxy (n :: Nat). (n `LeNat` Bound) ~ True => proxy n -> String
> f _ = "It worked!"
I'm happy to answer questions, but it's hard to know how much detail to use in
a description of the code.
I hope this helps,
Richard
On Dec 4, 2014, at 5:50 PM, Alexander V Vershilov
<alexander.vershi...@gmail.com> wrote:
> 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 <e...@cis.upenn.edu> 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
>> <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
>>>
>>
>
>
>
> --
> Alexander
>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
