CODEWITHSUNDEEP
haskelldependent-type
xiphoid
xiphoid

Reputation: 73

Haskell - How to define the dependent type Remainder (i.e. Rmndr modulo)?

My understanding is that the remainder type is a dependent type (depending on the modulo). I read about the DataKinds extension and was able to define it like the following:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs #-}
data Nat = Zero | Succ Nat

data Rmndr modulo where
    Nil :: Rmndr Zero
    Rmndr :: Integer -> Rmndr modulo

But then when I preceeded to implement the Eq class, I stuck at the condition

Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo)

because modulo is not a value, but a type. Even if we can write a function as follow:

decat :: Nat -> Integer
decat Zero = 0
decat (Succ nat) = decat nat + 1

we cannot use it as follows

instance Eq (Rmndr modulo) where
    Nil == Nil = True
    Rmndr x == Rmndr y =
        x `mod` (decat modulo) == y `mod` (decat modulo)

because "modulo" in this syntax is not a variable.

Can any one help on this puzzle? Thanks a lot!

Upvotes: 3

Views: 209

Answers (1)

Tikhon Jelvis
Tikhon Jelvis

Reputation: 68152

The trick is to use a typeclass to associate each natural number type with a singleton value. We do this by creating an instance for Zero associating with 0 and a recursive instance for Succ x. To access the type itself, we need to take a dummy proxy argument. The idiom for proxy arguments is to use a type variable called proxy a; when you go to call this, you would most often use Proxy from Data.Proxy.

Here's the relevant class:

class SingNat n where
  sing :: proxy n -> Integer

and the instances:

instance SingNat Zero where sing _ = 0

instance SingNat n => SingNat (Succ n) where
  sing _ = 1 + sing (Proxy :: Proxy n)

To make all of this work, you also have to enable ScopedTypeVariables which ensures the n in :: Proxy n is the same as the one in SingNat (Succ n).

A good intuition here is that the two typelcass instances are like the two cases of your decat function, but at the typelevel. Typeclasses used like this function as a little typelevel logic programming language, not unlike a mini Prolog.

Now you can use sing to get the modulo bound in your definition of Eq (and elsewhere):

instance SingNat n => Eq (Rmndr n) where
  Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo)
    where modulo = sing (Proxy :: Proxy n)

This sort of code is a great way to get the hang of type level programming. However, in real code, you probably don't want to roll your own natural number type because GHC has one built-in with DataKinds. Apart from being standard, this also gives you some syntax sugar at the type level letting you write types like Rmndr 10. If you're curious about this approach, take a look at my modular-arithmetic package, which implements your reminder type but using the built-in type level numbers and some nicer syntax. The code is short, so just read the source.

Upvotes: 5

Related Questions