[Haskell-cafe] Computed promoted natural
ariep at xs4all.nl
Fri Nov 9 17:06:07 CET 2012
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'
> 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?
More information about the Haskell-Cafe