小编rom*_*anb的帖子

定义case类时,默认的伴随对象有一个很好的curried方法来获取case类构造函数的curried版本:

scala> case class Foo(a: String, b: Int)
defined class Foo

scala> Foo.curried
res4: String => (Int => Foo) = <function1>

但是,只要我定义了一个显式的伴随对象,这个方法就会消失:

scala> :paste
// Entering paste mode (ctrl-D to finish)

case class Foo(a: String, b: Int)
object Foo {}

// Exiting paste mode, now interpreting.

defined class Foo
defined module Foo

scala> Foo.curried
<console>:9: error: value curried is not a member of object Foo
              Foo.curried

我可以这样回来:

scala> :paste
// Entering paste mode (ctrl-D to finish)

case class …

出于教育目的,我一直在尝试通过使用各种语言扩展和单例类型来重构Haskell中的"使用Idris进行类型驱动开发"(即RemoveElem.idr)一书中的示例.它的要点是一个从非空向量中移除元素的函数,给出了元素实际上在向量中的证明.以下代码是自包含的(GHC 8.4或更高版本).问题出现在最后:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind
import Data.Type.Equality
import Data.Void

-- | Inductively defined natural numbers.
data Nat = Z | S Nat deriving (Eq, Show)

-- | Singleton types for natural numbers.
data SNat :: Nat -> Type where
    SZ :: SNat 'Z …