haskell约束族

Rou*_*len 3 haskell types

我开始尝试使用GHC 7.4.2中的新类约束扩展,但是我遇到了一些问题,让一个小例子起作用.代码如下:

{-# LANGUAGE UndecidableInstances,
         MultiParamTypeClasses,
         KindSignatures,
         TypeFamilies,
         Rank2Types,
         ConstraintKinds,
         FlexibleInstances,
         OverlappingInstances #-}

module Test where

  import GHC.Exts  -- to get Constraint type constructor

  class NextClass f where
    type Ctxt f a :: Constraint
    next :: (Ctxt f a) => a -> a

  instance NextClass Int where
    type Ctxt Int a = Num a
    next b = b + 1

  n :: (NextClass a) => a -> a
  n v = next v
Run Code Online (Sandbox Code Playgroud)

我想要做的是定义一个NextClass类型类,它允许我(给定值x)获取所有类型的x的下一个值NextClass.要使用+运算符,我需要Num a类约束Int.

但是,GHC给了我以下错误:

Could not deduce (Ctxt f0 a) arising from a use of `next'
from the context (NextClass a)
   bound by the type signature for n :: NextClass a => a -> a
In the expression: next v
In an equation for `n': n v = next v
Run Code Online (Sandbox Code Playgroud)

我怀疑GHC告诉我它没有足够的信息来确定使用哪个约束族实例.

有人可以解释我在这里做错了什么.这是否正确使用约束族?

TIA

Dan*_*ner 5

你的定义中有一些奇怪的事情发生了.首先,类变量f从未在(仅)类方法的类型中提及next.编译器应该如何选择要使用的类型类实例?我假设你的意思是:

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
module Test where

import GHC.Exts  -- to get Constraint type constructor

class NextClass f where
    type Ctxt f :: Constraint
    next :: Ctxt f => f -> f

instance NextClass Int where
    type Ctxt Int = Num Int
    next b = b + 1

n :: (NextClass a) => a -> a
n v = next v
Run Code Online (Sandbox Code Playgroud)

下一个奇怪的是Int已经有一个Num实例,所以这不是一个约束.但是现在让我们把它放在一边(因为它不会影响我们得到的错误),只看一下新的错误:

test.hs:15:7:
    Could not deduce (Ctxt a) arising from a use of `next'
    from the context (NextClass a)
      bound by the type signature for n :: NextClass a => a -> a
      at test.hs:15:1-12
    In the expression: next v
    In an equation for `n': n v = next v
Run Code Online (Sandbox Code Playgroud)

实际上,这个错误看起来很明智:约束的全部意义在于拥有一个实例NextClass a是不够的; 我们还必须有一个实例Ctxt a.所以我们可以修复类型签名:

n :: (NextClass a, Ctxt a) => a -> a
n v = next v
Run Code Online (Sandbox Code Playgroud)

......然后编译.最后一个奇怪的是,这是一种特别简单的约束种类使用,因为这个更简单的代码基本上是等价的:

class NextClass f where
    next :: f -> f

instance Num Int => NextClass Int where
    next b = b + 1
Run Code Online (Sandbox Code Playgroud)

...从前一个东西到新东西的翻译是非常机械的:而不是声明instance NextClass {- foo -} where type Ctxt {- foo -} = {- bar -},你只需要写instance {- bar -} => NextClass {- foo -}.