[Haskell-cafe] Type-level Nat to Integer

[Andres Löh]

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