[Haskell-cafe] Infer Nat type from Integer argument
adam vogt
vogt.adam at gmail.com
Sun Feb 28 22:42:33 UTC 2016
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/20160228/eab3ad8e/attachment.html>
More information about the Haskell-Cafe
mailing list