2014-07-04 0:04 GMT+02:00 Andras Slemmer <0slemi0@gmail.com>:

Also, check out the singletons library, it handles type promotion/demotion pretty well. In particular the https://hackage.haskell.org/package/singletons-1.0/docs/Data-Singletons.html... typeclass handles demotion with fromSing

It's a little bit complicated for me at the time, but I'll have a look.

On 3 July 2014 14:39, Andres Löh wrote:

...

Hi.

In

...

class NatToInt n where natToInt :: n -> Int

the class parameter is of kind "Nat", but a function argument has to be of kind "*". However, you only want the "n" argument in order to "guide" the instance resolution mechanism. For this, you can use a "Proxy". A Proxy is a datatype that is parameterized by an arbitrary argument (of arbitrary kind), but has only one value, also called "Proxy", so it's perfect for an argument that has no computational meaning and is just there to make the type checker happy:

...

{-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds, ScopedTypeVariables #-}

import Data.Proxy

data Nat = Z | S Nat

class NatToInt n where natToInt :: Proxy n -> Int

instance NatToInt Z where natToInt _ = 0

instance NatToInt n => NatToInt (S n) where natToInt _ = 1 + natToInt (Proxy :: Proxy n)

Cheers, Andres

-- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Thanks (I finally understand the usefulness of Proxy).

You probably want the ScopedTypeVariables extension. You'll also have to qualify the relevant variable with an explicit forall: forall l. NatToInt l => ... Then you can use l in your expression and it will be in scope. On Jul 4, 2014 12:25 AM, "Gautier DI FOLCO" wrote:

2014-07-04 8:57 GMT+02:00 Gautier DI FOLCO :

...

2014-07-04 0:04 GMT+02:00 Andras Slemmer <0slemi0@gmail.com>:

Also, check out the singletons library, it handles type

...

promotion/demotion pretty well. In particular the https://hackage.haskell.org/package/singletons-1.0/docs/Data-Singletons.html... typeclass handles demotion with fromSing

It's a little bit complicated for me at the time, but I'll have a look.

...

On 3 July 2014 14:39, Andres Löh wrote:

...

Hi.

In

...

class NatToInt n where natToInt :: n -> Int

the class parameter is of kind "Nat", but a function argument has to be of kind "*". However, you only want the "n" argument in order to "guide" the instance resolution mechanism. For this, you can use a "Proxy". A Proxy is a datatype that is parameterized by an arbitrary argument (of arbitrary kind), but has only one value, also called "Proxy", so it's perfect for an argument that has no computational meaning and is just there to make the type checker happy:

...

{-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds, ScopedTypeVariables #-}

import Data.Proxy

data Nat = Z | S Nat

class NatToInt n where natToInt :: Proxy n -> Int

instance NatToInt Z where natToInt _ = 0

instance NatToInt n => NatToInt (S n) where natToInt _ = 1 + natToInt (Proxy :: Proxy n)

Cheers, Andres

-- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Thanks (I finally understand the usefulness of Proxy).

I have an additional question: How can I "extract" a type variable? I want to do something like this:

data Vector :: Nat -> * -> * where Nil :: Vector Z a El :: a -> Vector n a -> Vector (S n) a

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

Thanks in advance for your answers.

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

On Jul 4, 2014, at 9:39 AM, Gautier DI FOLCO wrote:

2014-07-04 9:30 GMT+02:00 Tikhon Jelvis : You probably want the ScopedTypeVariables extension. You'll also have to qualify the relevant variable with an explicit forall:

forall l. NatToInt l => ...

Then you can use l in your expression and it will be in scope.

Interesting, what it's the semantic which force me to add an explicit for all?

In the case you want to be _less_ general. That is, in you original code:

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

the two 'l' variables are not necessarily the same, that is, the compiler sees your code as:

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l1)

Notice that there are now two type variables, 'l' and 'l1', which is a more general function. In you case however, you want the 'l' in the where clause to be the same as the 'l' in your top-level type signature. So then you write:

lengthV :: forall l . NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

Which is less general, but exactly what you want. -- Christiaan

On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO wrote:

data Vector :: Nat -> * -> * where Nil :: Vector Z a El :: a -> Vector n a -> Vector (S n) a

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

You can do this without ScopedTypeVariables using a small helper function: lengthV :: NatToInt l => Vector l a -> Int lengthV = natToInt . (const Proxy :: Vector l' a' -> Proxy l') Note that this function is again polymorphic, hence no ScopedTypeVariables required.