# [Haskell-cafe] Infer Nat type from Integer argument

Mon Feb 29 20:14:06 UTC 2016

```Hi Jake,

On 29/02/16 01:42, Jake wrote:
> 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.

Exactly.

> Is there any way to signal that
> to the compiler without the extra overhead?

Not in GHC Haskell, unfortunately. Some compilers/languages introduce
existential types using a separate quantifier "exists", dual to
"forall", for exactly this purpose. For example, UHC [1] supports such
types. However, existentials complicate type inference, which is why GHC
requires the use of an explicit existential datatype (or the higher-rank

Hope this helps,

[1]
http://foswiki.cs.uu.nl/foswiki/Ehc/UhcUserDocumentation#A_3.6_Existential_types

> On Sun, Feb 28, 2016 at 5:42 PM adam vogt <vogt.adam at gmail.com
>
>     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,