You can only construct such a Proxy if you hide the type itself in an existential type. Take a look at Data.Singletons, specifically the toSing function for Nat/Integer. However what you will probably find is that a Proxy like that would not be useful at all in this case. What are you *really* trying to do? If you will only know the index (and the type of the element) at runtime then what you really need is dynamic typechecking. With the Typeable constraint you can do exactly that. Take a look at Data.Typeable's 'cast' function to dynamically safely coerce your unknown data into a known element type of the HList. On 23 December 2014 at 10:52, Erik Hesselink wrote:

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe