<div dir="ltr"><div><div><div><div><div><div><div><div>Hi Jake,<br><br></div><div>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:<br></div><div><br></div><div></div><div>1. make `fromN :: Integer -> SomeNatString`, making use of GADTs/ ExistentialQuantification (in the same way that SomeNat does):<br></div><br></div>data SomeNatString where<br></div> SomeNatString :: KnownNat n => NatString n -> SomeNatString<br><br></div>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:<br></div><div><br></div>fromN :: Integer -> (forall n. KnownNat n => Proxy n -> r) -> r<br></div>fromN i f = case someNatVal i of Just n -> f n<br><br></div>Regards,<br></div>Adam<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 28, 2016 at 4:40 PM, Jake <span dir="ltr"><<a href="mailto:jake.waksbaum@gmail.com" target="_blank">jake.waksbaum@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div style="font-size:13px;line-height:19.5px"><div>{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables, GADTs, AllowAmbiguousTypes #-}</div><div><br></div><div>import GHC.TypeLits</div><div>import Data.Proxy</div><div>import Data.Type.Equality</div><div><br></div><div>data NatString (n :: Nat) = NatString String deriving Show</div><div><br></div><div>showNS :: KnownNat n => NatString n -> (String, Integer)</div><div>showNS b@(NatString s) = (s, natVal b)</div><div><br></div><div>In this example, we use NatString like this:</div><div><br></div>> showNS (NatString "hey" :: NatString 4)</div><div style="font-size:13px;line-height:19.5px"><div>-- ("hey", 4)</div><div><br></div></div><div style="font-size:13px;line-height:19.5px">We can then dynamically make NatStrings from Integers. For example, we can read an Integer from stdin and use it to create a NatString</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>main :: IO ()</div><div>main = do</div><div> i <- readLn</div><div> case someNatVal i of</div><div> Just (SomeNat (p :: Proxy n)) -></div><div> let ns :: NatString n</div><div> ns = NatString "hello!"</div><div> in print $ showNS NatString</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">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.</div><div style="font-size:13px;line-height:19.5px">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.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>fromN :: forall n. KnownNat n => Integer -> NatString n</div><div>fromN i =</div><div> case someNatVal i of</div><div> Just (SomeNat p) -></div><div> case sameNat p (Proxy :: Proxy n) of</div><div> Just (Refl) -></div><div> let ns :: NatString n</div><div> ns = NatString "hello!" in ns</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">This compiles, but if you try and use it the compiler complains.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">> showNS<span style="color:rgb(0,0,0)"> (fromN 3)</span></div><div style="font-size:13px;line-height:19.5px">-- <span style="color:rgb(0,0,0)">No instance for (KnownNat n0) arising from a use of ‘showNS’</span></div><div style="font-size:13px;line-height:19.5px"><span style="color:rgb(0,0,0)"><br></span></div><div style="font-size:13px;line-height:19.5px"><span style="color:rgb(0,0,0)">If we manually add the type annotation, everything is fine, but that kind of defeats the entire purpose.</span></div><br style="font-size:13px;line-height:19.5px"><span style="font-size:13px;line-height:19.5px">> showNS (fromN 3 :: NatString 3)</span><br style="font-size:13px;line-height:19.5px"><span style="font-size:13px;line-height:19.5px">-- ("hello!",3)</span><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">Strangely enough, when the NatString is immediately consumed instead of being returned, the compiler does its job and infers the correct type.</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px"><div>showFromN :: Integer -> (String, Integer)</div><div>showFromN i =</div><div> case someNatVal i of</div><div> Just (SomeNat (p :: Proxy n)) -></div><div> let ns :: NatString n</div><div> ns = NatString "hello!" in showNS ns</div></div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">> showFromN 3</div><div style="font-size:13px;line-height:19.5px">-- ("hello!", 3)</div><div style="font-size:13px;line-height:19.5px"><br></div><div style="font-size:13px;line-height:19.5px">Clearly the intermediate value of ns inside of showFromN has a type NatString 3 because showNS is using that fact.</div><div style="font-size:13px;line-height:19.5px">How can I make the compiler infer that fromN 3 :: NatString 3 separately?</div></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>