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

Erik Hesselink hesselink at gmail.com
Tue Dec 23 09:52:17 UTC 2014


Hi Phil,

As you kind of figured out, it's not clear what the type of your
function intoToHNatProxy should be. The output type depends on the
input *value*, which requires dependent types. Haskell doesn't have
those (yet?). I think the best you can do is put the result in an
existential, in effect saying "this has *some* type, but I don't know
which one". Something like the code below. The problem is that what
you can then do with the value inside the existential is more limited.
It might help to know what the bigger picture is of what you're trying
to do.

{-# LANGUAGE GADTs #-}
import Control.Applicative
import Data.HList

data SomeHList where
  SomeHList :: HList l -> SomeHList

updateAtSomeN :: Int -> e -> HList l -> Maybe SomeHList
updateAtSomeN _ _ HNil         = Nothing
updateAtSomeN 0 e (HCons _ xs) = Just $ SomeHList (HCons e xs)
updateAtSomeN n e (HCons x xs) = consSomeHList x <$> updateAtSomeN (n - 1) e xs

consSomeHList :: e -> SomeHList -> SomeHList
consSomeHList x (SomeHList l) = SomeHList (HCons x l)

Erik

On Mon, Dec 22, 2014 at 1:59 AM, 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


More information about the Haskell-Cafe mailing list