递归方法如何工作？

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.考虑到这一点:

1. 我完全不明白如何调度方法.我会理论化,或者:

   • 表格形式(类型,方法名称)⟶功能由编译器生成.然后,在运行时,所有对象都使用其类型进行标记,而方法是一个高阶函数,它查看类型标记并在表中查找相应的函数.但人们说在编译过程中类型被完全删除,所以这并没有加起来.
   • 表格形式方法名称⟶函数附加到每个对象,方法调用表示为方法名称.然后,函数应用程序查找相应的Function并在强制它时应用它.为了节省空间,该表可以由该类型的所有成员共享,但是与使用类型标记的对象没有区别.
   • 表格形式(方法名称,实例索引)⟶函数由编译器生成,表格(方法名称 - >实例索引)在运行时附加到对象.这意味着对象不知道它的类型,但知道它所属的类,以及正确的实例选择.我不知道这种方法是否有任何好处.

    

   因此,如果对象未以某种方式(直接或间接)标记其类型,我不明白运行时系统如何确定方法实例的正确选择.周围的人都在谈论一些字典传递的东西,但我完全不明白:

   • 有什么关键？
   • 有什么价值？
   • 字典在哪里？(在堆上,在程序文本中,仍然在其他地方？)
   • 谁有指向字典的指针？

   ...等等.

2. 即使存在允许选择方法实例而不用类型标记对象的技巧,也只有2个实例Count,因此方法的选择可能只携带1位信息.(例如,可能Proxy有一个标签显示"将方法从实例A _1应用到我",并且A _1中的方法实例Proxy使用"将实例A _0中的方法应用于我"来重新标记.)这显然不是足够.运行时必须有一些东西在每次应用递归实例时都会下降.

您能指导我执行此代码,还是引入一些描述运行时系统适用细节的链接？

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

Answer 2

类型类被去掉了记录.一切都在编译时发生.

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

每当我们调用时count :: Count n => n -> Int,desugarer(在typechecker之后运行)查看推断类型n,并尝试构造类型的记录Count n.

因此,如果我们编写count (Proxy :: Proxy (S (S (S Z)))),我们需要一个类型的记录,Count (S (S (S Z)))唯一匹配的实例是Count (Proxy n) -> Count (Proxy (S n)),with n ~ S (S Z).这意味着我们现在必须构造其参数,类型Count (Proxy (S (S Z)))等等.

请注意,这也是count在实例中去除应用程序的过程中发生的情况Proxy (S n).

在此过程之后,没有类型类,一切都只是记录.