headers
Arie Peterson | 8 Nov 2012 16:54
Picon
Picon
Favicon

Computed promoted natural

Hi,

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.
(Continue reading)

Permalink | Reply |
headers
Ertugrul Söylemez | 8 Nov 2012 17:15
Picon
Gravatar

Re: Computed promoted natural

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
(Continue reading)

Permalink | Reply |
headers
Arie Peterson | 9 Nov 2012 17:06
Picon
Picon
Favicon

Re: Computed promoted natural

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
(Continue reading)

Permalink | Reply |
headers
Ertugrul Söylemez | 9 Nov 2012 17:53
Picon
Gravatar

Re: Computed promoted natural

Arie Peterson <ariep <at> xs4all.nl> wrote:

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

I'm not sure if you're supposed to use the reflection library that way.
The idea is simply this:

    reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r

You pass in a value, any value you like actually ('reify' is fully
polymorphic in 'a'), and the continuation receives a proxy that contains
a type that represents that value.  You can then use the 'Reifies' class
to recover the original value from the type 's'.  This goes with almost
no runtime cost.

In particular you should not write Reifies instances yourself.  Let's
say you want to write a data type for modular arithmetic that encodes
the modulus in its type:

    {-# LANGUAGE ScopedTypeVariables #-}

    import Data.Proxy
    import Data.Reflection
    import Text.Printf

    data Mod n a = Mod !a !a

    instance (Integral a) => Eq (Mod n a) where
        Mod n x == Mod _ y = mod (x - y) n == 0
(Continue reading)

Permalink | Reply |
headers
Arie Peterson | 9 Nov 2012 18:19
Picon
Picon
Favicon

Re: Computed promoted natural

On Friday 09 November 2012 17:53:54 Ertugrul Söylemez wrote:

> I'm not sure if you're supposed to use the reflection library that way.
> The idea is simply this:
> 
>     reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r
> 
> You pass in a value, any value you like actually ('reify' is fully
> polymorphic in 'a'), and the continuation receives a proxy that contains
> a type that represents that value.  You can then use the 'Reifies' class
> to recover the original value from the type 's'.  This goes with almost
> no runtime cost.
> 
> In particular you should not write Reifies instances yourself.  Let's
> say you want to write a data type for modular arithmetic that encodes
> the modulus in its type:
> […]

OK, thanks for the example. So, in this approach, we drop the type parameter 
'd' of kind 'Nat', and instead work with an type variable of kind *.

Thanks and regards,

Arie

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
(Continue reading)

Permalink | Reply |
headers
Arie Peterson | 10 Nov 2012 17:37
Picon
Picon
Favicon

Re: Computed promoted natural

On Friday 09 November 2012 17:53:54 Ertugrul Söylemez wrote:

> I'm not sure if you're supposed to use the reflection library that way.
> The idea is simply this: […]

All right, I switched to this method, and it workes like a charm.

It is also more general than my attempt using data kinds, in the sense that it 
workes for any type of parameter, not just integers and strings.

Thanks for the advice.

Regards,

Arie

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Iavor Diatchki | 8 Nov 2012 18:34
Picon
Gravatar

Re: Computed promoted natural

Hello Arie,


One way to achieve the additional static checking is to use values of type `Sing (n :: Nat)` in the places where you've used `Integer` (and parameterize data structures by the `n`).  If the code is fully polymorphic in the `n`, then you can use it with values whose types as not statically know by using an existential.  Here is an example:

{-# LANGUAGE DataKinds, KindSignatures, ExistentialQuantification #-}

import GHC.TypeLits

data SomeNat = forall (n :: Nat). SomeNat (Sing n)

getSomeNat :: IO SomeNat
getSomeNat =
  do x <- getLine
     case reads x of
       -- The use of `unsafeSingNat` is OK here because it is wrapped in `SomeNat`
       -- so we are not assuming anything about the actual number.
       [(n,_)] | n >= 0 -> return $ SomeNat $ unsafeSingNat n
       _ -> putStrLn "Invalid number, try again." >> getSomeNat

main :: IO ()
main =
  do x <- getSomeNat
     case x of
       SomeNat s -> polyFun s s

-- The argument of this function are always going to be the same.
-- (just an example, one could probably get more interesting properties)
polyFun :: Sing (n :: Nat) -> Sing n -> IO ()
polyFun x y = print (x,y)

I can elaborate more, just ask if this does not make sense.   One issue at the moment is that you have to pass the explicit `Sing` values everywhere, and it is a lot more convenient to use the `SingI` class in GHC.TypeLits.  Unfortunately at the moment this only works for types that are statically known at compile time.  I think that we should be able to find a way to work around this, but we're not quite there yet.

-Iavor






On Thu, Nov 8, 2012 at 7:54 AM, Arie Peterson <ariep <at> xs4all.nl> wrote:
Hi,


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.

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

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

However, it feels as though it might not be unreasonable in this situation,
because the computation is polymorphic in the type 'd :: Nat'. I just want to
substitute a specific value for 'd'.


Maybe there is another way to approach this?


Thanks for any advice,

Arie


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Arie Peterson | 9 Nov 2012 17:01
Picon
Picon
Favicon

Re: Computed promoted natural

Hello Iavor,

> One way to achieve the additional static checking is to use values of type
> `Sing (n :: Nat)` in the places where you've used `Integer` (and
> parameterize data structures by the `n`).  If the code is fully polymorphic
> in the `n`, then you can use it with values whose types as not statically
> know by using an existential.  Here is an example:
> […]
> I can elaborate more, just ask if this does not make sense.

Thanks for the example, it is very clear.

> One issue at
> the moment is that you have to pass the explicit `Sing` values everywhere,
> and it is a lot more convenient to use the `SingI` class in GHC.TypeLits.

Right. Apart from the inconvenience, it seems this approach doesn't allow the 
'Num' instance that I'm after: I can define a 'Num' instance for this type 
containing the 'Sing (n :: Nat)', but only when 'd' is an instance of 'SingI'.

> Unfortunately at the moment this only works for types that are statically
> known at compile time.  I think that we should be able to find a way to
> work around this, but we're not quite there yet.

OK. If there is progress in this area, I would be very interested!

Thanks and regards,

Arie

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |

Gmane