类型和GADT

Question

我正在将一个几何库放在haskell中.我不打算发布它,它只是一个项目,我用来提高我的语言知识.

我有一个Local数据类型,具有以下定义

data Local a where
    MkLocal :: (Vectorise a) => ReferenceFrame -> a -> Local a

参考框架是指向框架原点的矢量和表示框架旋转的角度,两者都定义为"绝对"参照系(嘿,它不是现实世界!).一个Vectorise几何是一个具有可逆转变成一个列表Vector.

在我看来,Local可以是Functor如下的实例:

instance Functor Local where
     fmap f geom = localise (frame geom) (f $ local geom)

但是编译器抱怨在定义中没有使用Vectorisable实例进行localize.有没有办法解决这个限制使用无数的GHC扩展之一？

编辑:根据评论中的要求,以下是一些使用的类型

local :: Local a -> a
frame :: Local a -> ReferenceFrame
localise :: (Vectorise a) => ReferenceFrame -> a -> Local a

错误是

No instance for (Vectorise b)
  arising from a use of `localise'
In the expression:
  localise (frame geom) (f $ local geom)
In an equation for `fmap':
    fmap f lgeom = localise (frame geom) (f $ local geom))
In the instance declaration for `Functor Local'

这是有道理的,因为类型fmap是(a -> b) -> f a -> f b.它可以推断出它a必须是一个实例Vectorise,但我想知道它是如何推断的那样b,除非我可以指定(不知何故)我可以告诉编译器f必须具有受限制的返回类型而不定义另一个类型类当已经有一个几乎已经适合该法案(或者,如果有人可以帮助解释为什么以这种方式限制类会以某种方式打破类型推断).

PS.我还修正了一个拼写错误,我在其定义中反转local和frame颠倒了fmap

Answer 1

问题是,localise需要它的第二个参数有型Vectorise a => a,但是当你申请f(其中有型a -> b)到的结果local(类型Vectorise a => a),也不能保证所得到的值将类型是的一个实例Vectorise.你真正想要的是一个类似的东西Functor只适用于有Vectorise约束的类型.

直到最近,才能定义这样的类型类.这是一个众所周知的问题,其原因是Data.Set没有Functor或Monad实例.然而,随着最近的ConstraintKindsGHC扩展,这种"限制仿函数"终于成为可能:

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

import GHC.Exts (Constraint)

data ReferenceFrame = ReferenceFrame

class Vectorise a where
  ignored :: a

data Local a where
    MkLocal :: ReferenceFrame -> a -> Local a

local :: Vectorise a => Local a -> a
local = undefined

frame :: Local a -> ReferenceFrame
frame = undefined

localise :: (Vectorise a) => ReferenceFrame -> a -> Local a
localise = undefined

class RFunctor f where
  type SubCats f a :: Constraint
  type SubCats f a = ()
  rfmap ::  (SubCats f a, SubCats f b) => (a -> b) -> f a -> f b

instance RFunctor Local where
  type SubCats Local a = Vectorise a
  rfmap f geom = localise (frame geom) (f $ local geom)

您可以ConstraintKinds 在这里和这里阅读更多相关信息.