haskell - 递归方法如何工作？

Question

考虑以下方法count将类型级别的自然数映射到值级别的自然数:

{-# 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)

它似乎在 repl 中工作:

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

要终止递归，在运行时必须有一些 Proxy 类型的指示。 ，但类型应该在运行时被删除。我什至可以替换 data与 newtype在 Proxy定义:

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

— 这将迫使它每次都具有相同的内存表示，因此它是 Coercible .考虑到这一点:

我完全不明白一个方法是如何被调度的。我会理论化，要么:

表格(类型、方法名称)⟶ 函数由编译器生成。然后，在运行时，所有对象都用它们的类型进行标记，方法是一个高阶函数，它查看类型标记并在表中查找相应的函数。但是人们说类型在编译过程中被完全删除，所以这并没有加起来。

每个对象都附有一个方法名⟶函数形式的表格，方法调用表示为方法名。然后，函数应用程序查找相应的函数并在强制执行时应用它。为了节省空间，该表可以由该类型的所有成员共享，但这与使用类型标记的对象没有什么不同。

表格(方法名称，实例索引)⟶函数由编译器生成，表格(方法名称->实例索引)在运行时附加到对象上。这意味着一个对象不知道它的类型，但知道它所属的类以及实例的正确选择。我不知道这种方法是否有任何优势。

所以，如果对象没有以某种方式直接或间接地用它们的类型标记，我不明白运行时系统如何确定方法实例的正确选择。周围的人都在谈论一些字典传递的东西，但我完全不明白:

什么是 key ？

值(value)观是什么？

字典在哪里？ (在堆上，在程序文本中，还是在别处？)

谁有字典的指针？

...等等。

即使有一个技巧允许选择方法实例而不用类型标记对象，也只有 2 个 Count 的实例。 ，因此方法的选择可能只携带 1 位信息。 (例如，可能有一个 Proxy 带有一个标签，上面写着“将实例 A1 中的方法应用到我”，而 A1 中的方法实例将 Proxy 重新标记为“将实例 A0 中的方法应用到我”。)这个显然是不够的。每次应用递归实例时，运行时都必须有一些东西在滴答作响。

你能引导我完成这段代码的执行，或者提供一些描述运行时系统的适用细节的链接吗？

Answer 1

每当在函数声明的 LHS 出现约束时，例如

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

它就像是语法糖

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

在哪里 CountDictionary a是一种适合运行时的(但单例——编译器总是为每种类型选择一个实例!)实际上是 Count 的方法的表示。类，即

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

在我进一步阐述之前，让我重写所有没有那些丑陋的代理以支持 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

现在当你写 count @(S(S(S Z))) ，它表示为

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)))) )