How does a recursive method work?

Question

Consider the following method count that maps type level natural numbers to value level ones:

{-# LANGUAGE
    DataKinds
  , KindSignatures
  , PolyKinds
  , FlexibleInstances
  , FlexibleContexts
  , ScopedTypeVariables
  #-}


module Nat where

data Nat = Z | S Nat

data Proxy (a :: k) = Proxy

class Count a where
    count :: a -> Int

instance Count (Proxy Z) where
    count _ = 0

instance Count (Proxy n) => Count (Proxy (S n)) where
    count _ = succ $ count (Proxy :: Proxy n)

It seems to work in repl:

λ count (Proxy :: Proxy (S(S(S Z))) )
3

For the recursion to terminate, there must be some indication at run time of the type of the Proxy, but types are supposed to be erased at run time. I can even replace data with newtype in the Proxy definition:

newtype Proxy (a :: k) = Proxy ()

— Which would oblige it to have the same memory representation every time, so that it were Coercible. With that in mind:

1. I totally do not understand how a method gets dispatched. I would theorize that, either:

   • A table of form (Type, Method name) ⟶ Function is generated by the compiler. Then, at run time, all the objects are tagged with their type, and a method is a higher order function that looks at the type tag and looks up the corresponding function in the table. But people say types are completely erased during compilation, so this does not add up.
   • A table of form Method name ⟶ Function is attached to every object, and a method invocation is represented as Method name. Then, a function application looks up the corresponding Function and applies it when it is forced. To save space, the table may be shared by all the members of the type, but then it is no different from having objects tagged with type.
   • A table of form (Method name, Instance index) ⟶ Function is generated by the compiler, and tables of form (Method name -> Instance index) are attached to objects at run time. This means an object does not know its type, but knows the classes it belongs to, and the correct choice of instance. I do not know if there are any advantages to this approach.

    

   So, I do not understand how the run time system determines the right choice for the method instance if the objects are not tagged with their type in some way, direct or indirect. People all around are talking about some dictionary passing stuff, but I totally do not get it:

   • What are the keys?
   • What are the values?
   • Where does the dictionary reside? (On the heap, in the program text, still elsewhere?)
   • Who has pointers to the dictionary?

   ...Et cetera.

2. Even if there is a trick in place that allows for the choice of method instance without tagging objects with types, there are only 2 instances of Count, so the choice of a method may only carry 1 bit of information. (For example, there may be a Proxy with a tag that says "apply methods from instance A₁ to me", and the method instance in A₁ retags the Proxy with "apply methods from instance A₀ to me".) This is clearly not enough. There must be something at run time that ticks down every time the recursive instance is applied.

Can you walk me through the execution of this code, or throw in some links that describe the applicable particulars of the runtime system?

Answer 1

Whenever a constraint turns up at the LHS of a function declaration, like

count :: (Count a) => a -> Int

it's as it were syntactic sugar for

count' :: CountDictionary a -> a -> Int

where CountDictionary a is a runtime-suitable (but singleton – the compiler always chooses exactly one instance for each type!) representation of, indeed, the methods of the Count class, i.e.

data CountDictionary a = CountDict {
         countMethod :: a -> Int
       }

Before I elaborate further, let me rewrite all without those ugly proxies in favour of TypeApplications:

{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, UnicodeSyntax #-}

class Count a where
    count :: Int
⇒ count' :: CountDictionary a -> Int
w/ data CountDictionary a = CountDict Int

instance Count Z where
    count = 0

instance ∀ n . Count n => Count (S n) where
    count = succ $ count @n

Now when you write count @(S(S(S Z))), it's represented by

count @(S(S(S Z)))
  = count' ( CountDict (succ $ count @(S Z)) )
  = count' ( CountDict (succ $ count' (CountDict (succ $ count @Z))) )
  = count' ( CountDict (succ $ count' (CountDict (succ $ count' (CountDict 0)))) )

Answer 2

Type classes are desugared to records. Everything happens at compile time.

data Count a = Count { count :: a -> Int }

instance_Count_ProxyZ :: Count (Proxy Z)
instance_Count_ProxyZ = Count { count = \_ -> 0 }

instance_Count_ProxySn :: Count (Proxy n) -> Count (Proxy (S n))
instance_Count_ProxySn context = Count {
  count = \_ -> succ (count context (Proxy :: Proxy n)) }

Whenever we call count :: Count n => n -> Int, the desugarer (that runs after the typechecker) looks at the inferred type for n, and tries to construct a record of type Count n.

So if we write count (Proxy :: Proxy (S (S (S Z)))), we need a record of type Count (S (S (S Z))), and the only matching instance is Count (Proxy n) -> Count (Proxy (S n)), with n ~ S (S Z). This means we now have to construct its argument, of type Count (Proxy (S (S Z))), and so on.

Note that this is also what happens in the process of desugaring the application of count in the instance for Proxy (S n).

After this process there are no type classes left, everything is just records.