[Haskell-cafe] Lifting a value into a DataKind

[Ivan Lazar Miljenovic]

On 10 February 2017 at 00:48, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> Ah. Now I get it!
>
> You originally described a type `a -> (forall b. Proxy (b :: a) -> r) -> r`, which doesn't seem very useful to me. The continuation function in there doesn't get any new information, so it can't make any decisions based on the choice of a. On the other hand, Erik's withLibrary has this type: `Library -> (forall (l :: Library). PutGet l => Proxy l -> k) -> k`. The key difference is that the continuation now has a constraint on it, which means a dictionary will be passed at runtime. Then, the proxy argument is useful, as it can be used to select the dictionary.
>
> So, perhaps this is what you want:
>
> with :: forall (a :: Type) (c :: a -> Constraint) (r :: Type). a -> (forall (b :: a). c b => Proxy b -> r) -> r
>
> `with` would look at the value of type `a` that has been provided, select a dictionary based on that choice, and then pass the dictionary to the continuation.
>
> Now, I can answer your original question: No, GHC can't do that. GHC internally is unaware of the relationship between, say, the value True and the type 'True. And even if it were, this would be a hard function to write, as it really does have to case-match at runtime to select the right dictionary. Given that the instances available might not exactly match the constructors of the type `a`, more processing might be necessary. It's conceivable, I suppose, that this ability could be baked in, but it would be non-trivial to do so.
>
> By the way, you're right that singletons is way too large a hammer for this. I would just do what Erik did. :)

Well, I wrote it in a pull request for Erik, but yes, it appears that
just writing it each time is easier :)

>
> Richard
>
>> On Feb 8, 2017, at 10:40 PM, Ivan Lazar Miljenovic <ivan.miljenovic at gmail.com> wrote:
>>
>> Yeah, Erik ended up reverting those changes.  Here's what it should
>> have been: https://github.com/ivan-m/fastpack/blob/ccf08a96e351b3a6ecac651971a1023f830c8f59/bench/bench.hs
>>
>> On 9 February 2017 at 13:31, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
>>> Is this the wrong link? I don't see any text matching compareFunc or withLibrary on that page... Sorry!
>>>
>>> Richard
>>>
>>>> On Feb 8, 2017, at 12:43 AM, Ivan Lazar Miljenovic <ivan.miljenovic at gmail.com> wrote:
>>>>
>>>> As a sample implementation of the current state that I'd like to
>>>> simplify, see https://github.com/erikd/fastpack/blob/master/bench/bench.hs
>>>> (specifically, the `compareFunc` usage and the definition of
>>>> `withLibrary`).
>>>
>>
>>
>>
>> --
>> Ivan Lazar Miljenovic
>> Ivan.Miljenovic at gmail.com
>> http://IvanMiljenovic.wordpress.com
>



-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic at gmail.com
http://IvanMiljenovic.wordpress.com