标签: constraint-kinds

我想要的

class Trivial t
instance Trivial t

这在Haskell 98中当然没用,因为你可以省略约束; 但ConstraintKinds我们可以明确要求种类的论点* -> Constraint.理想情况下,我想将其定义为"匿名类型级函数" \type a -> (),但这显然是不可能的.

我应该怎么做,使用预定义的东西或者只在我需要的地方定义该类(因为实例是通用的,没有人需要访问它,看起来也很好)？

什么是约束类型？

为什么有人会使用它(在实践中)？

到底有什么好处呢？

您能举一个简单的代码示例来说明前两个问题的答案吗？

例如,为什么在此代码中使用它？

Constraint当我尝试编写一个简单的例子时,我收到的错误不在范围内,

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

type family A a :: Constraint

错误是,

> ghci test.hs
[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:10:20: Not in scope: type constructor or class `Constraint'
Failed, modules loaded: none.

约束同义词似乎按预期工作,

type ShowOrd a = (Ord a, Show a)

提前致谢.

我们可以使用扩展ConstraintKinds来扩展基类型类的功能以允许约束.例如,我们可以将未装箱的矢量作为仿函数:

class Functor f where
    type FunctorConstraint f x :: Constraint
    type FunctorConstraint f x = ()
    fmap :: (FunctorConstraint f a, FunctorConstraint f b) => (a -> b) -> f a -> f b

instance Functor VU.Vector where
    type FunctorConstraint VU.Vector x = VU.Unbox x
    fmap = VU.map

(见这些博客 帖子有详细介绍).

我注意到自己在这种新风格中实现了相当大部分的基本库类型(基本上我希望能够在未装箱的向量和列表之间互换),并且我想知道是否已经存在我应该使用的库,或者如果我应该将我的肉体添加到hackage中.

编辑:此外,是否有计划将此直接添加到基地？它似乎不应该通过直接更新类定义来破坏其他任何东西.

显然有点心不在焉,我写了类似下面的内容:

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE TypeFamilies        #-}

class Foo f where
  type Bar f :: *
  retbar :: Bar f -> IO f

type Baz f = (Foo f, Eq f)

  -- WithBar :: * -> (*->Constraint) -> * -> Constraint
type WithBar b c f = (c f, Bar f ~ b)

instance Foo () where
  type Bar () = ()
  retbar = return

naim :: WithBar () Baz u => IO u  -- why …

如果我检查kind的Maybe,我得到这样的:

?> :k Maybe
Maybe :: * -> *

现在,如果我检查一下,Monad我得到这个:

?> :k Monad
Monad :: (* -> *) -> Constraint

有什么Constraint需要以及为什么需要它？为什么不* -> *呢？

我想在得分类型中实现动态编程算法多态; 这是一个没有边界条件的简化1D版本:

{-# LANGUAGE ConstraintKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}

import Control.Monad
import Control.Monad.ST.Strict
import Data.Array.ST
import Data.Array.Unboxed

dynamicProgrammingSTU
  :: forall e i . (
    IArray UArray e,
    forall s. MArray (STUArray s) e (ST s),
    Ix i
  )
  => (forall m . Monad m => (i -> m e) -> (i -> m e))
  -> (i, i)
  -> (i -> e)
dynamicProgrammingSTU prog bnds = (arr !) where
  arr :: UArray i e
  arr = runSTUArray resultArrayST

  resultArrayST :: forall …

当我在haskell中有如下数据类型时:

data A ctx = A (forall a. ctx a => a -> a)

然后我可以将处理给定类的类型值的函数放入此数据类型中:

> A (+3) :: A Num
A (+3) :: A Num :: A Num

但是也可以将具有多个约束的函数放入此数据类型中吗？我试过这个:

> :t ((+ 3) . succ)
((+ 3) . succ) :: (Enum c, Num c) => c -> c
> :t A ((+ 3) . succ) :: A (Enum,Num)
  Expecting one more argument to `Enum'
  In an expression type signature: A (Enum, Num)
  In the expression: A ((+ 3) . …

我可以写下面的内容:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}

f :: Integral a => (forall b. Num b => b) -> a
f = id

一切都很好.据推测GHC可以得到Integral从Num这样一切都很好.

我可以有点琐事,但我仍然很好:

class Integral x => MyIntegral x
instance Integral x => MyIntegral x

class Num x => MyNum x
instance Num x => MyNum x

f' :: MyIntegral a => (forall b. MyNum b => b) -> a
f' = id

所以我想说我想概括一下,如下: …

我想表达一个Constrainton types of kind k -> k -> Type，可以用英文表述为：

一种类型，s例如 forall x x'、y、 以及y'whereCoercible x x'和Coercible y y'、Coercible (s x y) (s x' y')

或者用更简单的英语：

s如果其两个参数是可强制转换的，则该类型始终是可强制转换的。

后者似乎已经非常接近 haskell，而且我有一些看起来确实应该这样做的代码：

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')

但是这不起作用，ghc 想要Coercible (s x y) (s …