1

我已经提升了 typeNat = Suc Nat | Zero并且我想创建一个 typeclass class C (a :: Nat) b。有没有办法说服 GHCinstance C Zero b并instance C (Seq x) b涵盖所有情况，因此每当我使用类的方法时，我都不需要显式声明C为约束。这是一些代码：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
-- Some of these may not be necessary for the particular snippet.

data Nat = Zero | Suc Nat
-- TypeApplications, I know. I am traditional.
data NProxy :: Nat -> * where
  NProxy :: NProxy n

class C (a :: Nat) b where
  f :: NProxy a -> b -> Maybe b

instance C Zero b where
  f _ _ = Nothing
instance C (Suc a) b where
  f _ = Just
-- instance C n b where
--   f = error "This should not have been reached using GetNum."


class C1 a where
  f1 :: a -> Maybe a

instance C1 a where
  f1 = Just

type family GetNum a :: Nat where
  GetNum Char = (Suc Zero)
  GetNum Int = Suc (Suc Zero)
  GetNum [x] = Suc (GetNum x)
  GetNum a = Suc Zero

-- Error:
-- • No instance for (C (GetNum a) a) arising from a use of ‘f’
-- • In the expression: f (NProxy :: NProxy (GetNum a)) x
--   In an equation for ‘noGreet’:
--       noGreet x = f (NProxy :: NProxy (GetNum a)) x
noGreet :: forall a . a -> Maybe a
noGreet x = f (NProxy :: NProxy (GetNum a)) x

-- This one works fine though.
dumb :: a -> Maybe a
dumb = f1

编辑：一个相关的问题是，考虑到注释掉的实例 if C，为什么当我noGreet "hi"对 repl 说我得到一个异常而不是Just "hi"。

4

1 回答 1

4 
noGreet :: forall a . a -> Maybe a

参数化表示这种类型的唯一可定义值是

noGreet x = Just x
noGreet x = Nothing
noGreet x = undefined
noGreet x = x `seq` Just x
...

我们不能做出任何依赖于类型的选择a，比如“ Nothingif ais Charelse Just x”。

a“欺骗类型检查器”是一个红鲱鱼，因为阻止您编写这样一个函数的不是类型检查器，而是关于类型的信息在运行时根本不可用的事实。

当你用IncoherentInstances在

noGreet :: forall a . a -> Maybe a
noGreet x = f (NProxy :: NProxy (GetNum a)) x

编译器必须选择C使用哪个实例来调用f，因为 . 的类型中没有提供上下文noGreet。当然，唯一申请的是

instance C n b where f = error "This should not have been reached using GetNum."

因为当我们对a.

于 2017-02-14T15:26:58.350 回答