[Haskell-cafe] Infer Nat type from Integer argument

[Jake]

Thanks for the help!

So In both solutions, the goal is to "hide" the n so that the caller
doesn't determine it, right?

I think I understand why that's necessary: because given a function with
type signature

fromN :: forall n. KnownNat n => Integer -> NatString n

it looks like n is free to be determined, even though n will/should be
decided based on the Integer argument. Is there any way to signal that to
the compiler without the extra overhead?

On Sun, Feb 28, 2016 at 5:42 PM adam vogt <vogt.adam at gmail.com> wrote:

> Hi Jake,
>
> I think your problem is that the type signature for fromN lets the caller
> of fromN decide what n should be, when it has to be the other way around.
> Two ways to express that are:
>
> 1. make `fromN :: Integer -> SomeNatString`, making use of GADTs/
> ExistentialQuantification (in the same way that SomeNat does):
>
> data SomeNatString where
>  SomeNatString :: KnownNat n => NatString n -> SomeNatString
>
> 2. use RankNTypes to express the same thing without adding a constructor,
> but at the cost of needing to write a type signature and continuation
> passing style code:
>
> fromN :: Integer -> (forall n. KnownNat n => Proxy n -> r) -> r
> fromN i f = case someNatVal i of Just n -> f n
>
> Regards,
> Adam
>
> On Sun, Feb 28, 2016 at 4:40 PM, Jake <jake.waksbaum at gmail.com> wrote:
>
>> {-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, GADTs,
>> AllowAmbiguousTypes #-}
>>
>> import GHC.TypeLits
>> import Data.Proxy
>> import Data.Type.Equality
>>
>> data NatString (n :: Nat) = NatString String deriving Show
>>
>> showNS :: KnownNat n => NatString n -> (String, Integer)
>> showNS b@(NatString s) = (s, natVal b)
>>
>> In this example, we use NatString like this:
>>
>> > showNS (NatString "hey" :: NatString 4)
>> -- ("hey", 4)
>>
>> We can then dynamically make NatStrings from Integers. For example, we
>> can read an Integer from stdin and use it to create a NatString
>>
>> main :: IO ()
>> main = do
>>   i <- readLn
>>   case someNatVal i of
>>     Just (SomeNat (p :: Proxy n)) ->
>>       let ns :: NatString n
>>           ns = NatString "hello!"
>>       in print $ showNS NatString
>>
>> However, if I have trouble when I try to refactor out the middle part to
>> create a function with type forall n. KnownNat n => Integer -> Bar n.
>> I use sameNat to convince the compiler that the Nat we get from the
>> Integer is the same type as the the type n of the output.
>>
>> fromN :: forall n. KnownNat n => Integer -> NatString n
>> fromN i =
>>  case someNatVal i of
>>    Just (SomeNat p) ->
>>      case sameNat p (Proxy :: Proxy n) of
>>        Just (Refl) ->
>>          let ns :: NatString n
>>              ns = NatString "hello!" in ns
>>
>> This compiles, but if you try and use it the compiler complains.
>>
>> > showNS (fromN 3)
>> -- No instance for (KnownNat n0) arising from a use of ‘showNS’
>>
>> If we manually add the type annotation, everything is fine, but that kind
>> of defeats the entire purpose.
>>
>> > showNS (fromN 3 :: NatString 3)
>> -- ("hello!",3)
>>
>> Strangely enough, when the NatString is immediately consumed instead of
>> being returned, the compiler does its job and infers the correct type.
>>
>> showFromN :: Integer -> (String, Integer)
>> showFromN i =
>>  case someNatVal i of
>>    Just (SomeNat (p :: Proxy n)) ->
>>      let ns :: NatString n
>>          ns = NatString "hello!" in showNS ns
>>
>> > showFromN 3
>> -- ("hello!", 3)
>>
>> Clearly the intermediate value of ns inside of showFromN has a type
>> NatString 3 because showNS is using that fact.
>> How can I make the compiler infer that fromN 3 :: NatString 3 separately?
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160229/6fa5abc5/attachment.html>