[Haskell-cafe] Infer Nat type from Integer argument

[Adam Gundry]

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
encoding) instead.

Hope this helps,

(another) Adam

[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
> <mailto:vogt.adam at gmail.com>> 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



-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/