[Haskell-cafe] Computed promoted natural

[Ertugrul Söylemez]

Arie Peterson <ariep at xs4all.nl> wrote:

> I'm trying to use data kinds, and in particular promoted naturals, to
> simplify an existing program.
>
> The background is as follows: I have a big computation, that uses a
> certain natural number 'd' throughout, which is computed from the
> input. Previously, this number was present as a field in many of my
> data types, for instance
>
> > data OldA = OldA Integer …
>
> . There would be many values of this type (and others) floating
> around, with all the same value of 'd'. I would like to move this
> parameter to the type level, like this:
>
> > data NewA (d :: Nat) = NewA …
>
> The advantage would be, that the compiler can verify that the same
> value of 'd' is used throughout the computation.
>
> Also, it would then be possible to make 'NewA' a full instance of
> 'Num', because 'fromInteger :: Integer -> NewA d' has a natural
> meaning (where the value of 'd' is provided by the type, i.e. the
> context in which the expression is used), while 'fromInteger ::
> Integer -> OldA' does not, because it is not possible to create the
> right value of 'd' out of thin air.
>
> Is this a sane idea? I seem to get stuck when trying to /use/ the
> computation, because it is not possible to create 'd :: Nat', at the
> type level, from the computed integer.

This is a known and nice way to do it, and not just possible, but
actually quite beautiful.  It all revolves around two related concepts
called reflection and reification, the latter allowing precisely what
you think is impossible:

    {-# RankNTypes, ScopedTypeVariables #-}

    reflectNum :: (Num a, ReflectNum n) => proxy n -> a

    reifyNum ::
        (Num a)
        => a
        -> (forall n. (ReflectNum n) => Proxy n -> b)
        -> b


> Can one somehow instantiate the type variable 'd :: Nat' at an
> integer that is not statically known?

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:

    reifyNum 0 k = k (Proxy :: Proxy Z)
    reifyNum n k =
        reifyNum (n - 1) (\(_ :: Proxy n) ->
                              k (Proxy :: Proxy (S n)))

Reflection and reification together are part of a larger concept called
implicit configurations, and there is a paper about it.


> Formulated this way, it sounds like this should not be possible,
> because all types are erased at compile time.

The types are, but the type class dictionaries remain.

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).


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121108/63211c22/attachment.pgp>