[Haskell-cafe] Infer Nat type from Integer argument
Adam Gundry
adam at well-typed.com
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
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/
More information about the Haskell-Cafe
mailing list