Re: [Haskell-cafe] Type-level Nat to Integer

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.