[Haskell-cafe] How to call hUpdateAtHNat with a value known only at runtime

[adam vogt]

Hi Phil,

I think you're looking for a function that's sort of like:

> withInt :: Int -> (forall (n :: HNat). Proxy n -> r) -> r
> withInt 0 f = f hZero
> withInt n f = withInt (n-1) (f . hSucc)

But that one is pretty useless because you can't even supply
hNat2Integral as the second argument:

> withInt 5 hNat2Integral

    Could not deduce (HNat2Integral n)
      arising from a use of ‘hNat2Integral’
    from the context (Integral r)

That expression typechecks (and gives the value 5 back) if we add that
missing constraint:

> withInt :: Int -> (forall (n :: HNat). HNat2Integral n => Proxy n -> r) -> r

That's fine, but I don't have a solution for HUpdateAtHNat. The
problem is that the constraint you bring along has to work with any
'n' but HUpdateAtHNat doesn't typecheck if you try to update beyond
the end of the list, so when I write:

withIntUp :: HUpdateAtHNat HZero e l
      => Proxy '(e,l)
      -> Int
      -> (forall (n :: HNat). HUpdateAtHNat n e l => Proxy n -> r)
      -> r
withIntUp _ 0 f = f hZero
withIntUp p n f = withIntUp p (n-1) (f . hSucc)

There's a type error:

    Could not deduce (HUpdateAtHNat ('HSucc n) e l)
      arising from a use of ‘f’
    from the context (HUpdateAtHNat 'HZero e l)

Another sort of solution is http://lpaste.net/117131, but it's
unpleasant to put more things into an ApplyAB instance than you have
to.

Regards,
Adam

On Sun, Dec 21, 2014 at 7:59 PM, Phil Darnowsky <phil at darnowsky.com> wrote:
> Hello all,
>
> I'm working on something that involves HLists where I'm making use of the
> hUpdateAtHNat function for array-like semantics, which works great if you
> know the index of the element you want at compile time:
>
> Prelude> :module +Data.HList
>
> Prelude Data.HList> let hl = hEnd $ hBuild "foobar" 123 True
> Loading [a bunch of packages]
>
> Prelude Data.HList> hl
> H["foobar", 123, True]
>
> Prelude Data.HList> hUpdateAtHNat hZero 90909 hl
> H[90909, 123, True]
>
> Prelude Data.HList> hUpdateAtHNat (hSucc hZero) 90909 hl
> H["foobar", 90909, True]
>
> Prelude Data.HList> hUpdateAtHNat (hSucc $ hSucc hZero) 90909 hl
> H["foobar", 123, 90909]
>
>
> So far so good. What's giving me trouble is figuring out how to update at an
> arbitrary index, where that index is only known at runtime, because hZero
> and hSucc are of different types:
>
> Prelude Data.HList> :t hZero
> hZero :: Proxy 'HZero
>
> Prelude Data.HList> :t hSucc hZero
> hSucc hZero :: Proxy ('HSucc 'HZero)
>
>
> What I'd ideally like is some kind of function intToHNatProxy that would
> take an Int and return a Proxy of the appropriate type, but I so far only
> kinda sorta understand how proxies and lifted types work, so I haven't yet
> succeeded in constructing one. Any advice would be very welcome.
>
> Thanks,
> Phil
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe