Re: [Haskell-cafe] Infer Nat type from Integer argument

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_t...

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