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

Hello, Have you tried using the package https://hackage.haskell.org/package/reflection ? It won't directly help you with: fromN :: forall n. KnownNat n => Integer -> NatString n but it does provide a function: reifyNat :: forall r. Integer -> (forall n. KnownNat n => Proxy n -> r) -> r which could help you if you'd manage to turn your function inside out, so that the `n` parameter doesn't escape the callback. Best regards, Marcin Mrotek