Re: [Haskell-cafe] Infer Nat type from Integer argument

28 Feb 2016

      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  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  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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe