2014-07-04 8:57 GMT+02:00 Gautier DI FOLCO <gautier.difolco@gmail.com>:

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#t:SingKind 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 <andres@well-typed.com> 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