[Haskell-cafe] Computed promoted natural

[Arie Peterson]

On Thursday 08 November 2012 17:15:49 Ertugrul Söylemez wrote:

| […]
| The idea is that reifyNum takes a polymorphic (!) function in 'n', such
| that the function can guarantee that it can handle any 'n', as long as
| it's an instance of ReflectNum.  Now since the argument function is
| polymorphic, the reifyNum function itself can choose the type based on
| whatever value you pass as the first argument:

OK. It's nice that this is possible. The polymorphism should logically suffice 
to do this, but I wasn't sure if one could express this in Haskell.

| Of course there is no reason to reinvent the wheel here.  Check out the
| 'reflection' library, which even uses some magic to make this as
| efficient as just passing the value right away (without
| Peano-constructing it).

Right. So, let's try to fit GHC's singleton types to the reflection library.

> import Data.Proxy
> import Data.Reflection
> import GHC.TypeLits
> 
> instance (SingI d,SingE d Integer) => Reifies (Sing d) Integer where
>   reflect (_ :: p (Sing d)) = fromSing (sing :: Sing d)

This works, by itself.

However, when trying to apply 'Data.Reflection.reify', I cannot create a 
polymorphic argument function 'f' that is polymorphic enough. I need the 
'SingI d' constraint in my 'f', while according to 'reify', the type of 'f' 
should be

> forall s. Reifies s a => Proxy s -> r

With this type, there is not enough known about 's' (no connection to the 
singleton types); the only thing you can do is apply 'reflect', but this only 
gives you an integer, leading back to the original problem.


So, what I seem to need is a reification function for GHC's singleton natural 
types. For example:

> reify :: Integer
>     -> (forall d. (SingI d) => c d)
>     -> (forall d. (SingI d) => c d -> r)
>     -> r

(Where the second argument creates some piece of data that depends on the 
value of 'd', and the third argument uses this data to compute a final answer.) 
Maybe there is a simpler or more fundamental reification function, but this one 
would work for my application.

Is this 'reify' possible?


Regards,

Arie