[Haskell-cafe] Lifting a value into a DataKind

[Richard Eisenberg]

I fear, though, that you'll need a big hammer to be able to do what you want. Could you draw out your example a bit, and then we can see what the smaller hammer might look like.

Richard

> On Feb 7, 2017, at 10:32 PM, Ivan Lazar Miljenovic <ivan.miljenovic at gmail.com> wrote:
> 
> Thanks for the suggestion; I think singletons is a bit of a large
> hammer for a small bit of extra functionality I was thinking of adding
> though (especially with people needing to use TH to make their
> datatypes instances of SingI as well).
> 
> On 8 February 2017 at 12:55, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
>> The singletons library's `toSing` (or `withSing`) may be what you want. Note that if you use Proxy, you won't be able to make any runtime decisions on the choice of `b`.
>> 
>> Richard
>> 
>>> On Feb 7, 2017, at 6:55 PM, Ivan Lazar Miljenovic <ivan.miljenovic at gmail.com> wrote:
>>> 
>>> Is it possible to automatically lift an arbitrary value into a type?
>>> i.e. I'm after a function of type `a -> Proxy (b :: a)`.
>>> 
>>> More specifically, I'm wanting to be able to write a function that can
>>> convert an Enum (e.g. Bool or Ord) into such a Proxy, so I can
>>> actually write a function that looks like: `a -> (forall b. Proxy (b
>>> :: a) -> r) -> r` and use the `a` type as a selector value (to e.g.
>>> choose between type class instances).
>>> 
>>> --
>>> Ivan Lazar Miljenovic
>>> Ivan.Miljenovic at gmail.com
>>> http://IvanMiljenovic.wordpress.com
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>> 
> 
> 
> 
> -- 
> Ivan Lazar Miljenovic
> Ivan.Miljenovic at gmail.com
> http://IvanMiljenovic.wordpress.com