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