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

[Phil Darnowsky]

Thanks Adam, Andras and Erik for the advice. I think I can get what I 
want here with the vector-heterogeneous library, if not I'll have to 
rethink my approach.

On 12/23/2014 11:01 PM, adam vogt wrote:
> 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