Typeclasses and GADTs
I'm putting together a geometry library in haskell. I'm not intending to release it, it's just a project that I'm using to improve my knowledge of the language.
I have a Local datatype, with the following definition
data Local a where
MkLocal :: (Vectorise a) => ReferenceFrame -> a -> Local a
A reference frame is a Vector pointing to the origin of the frame and an angle representing the rotation of the frame, both defined wrt the "absolute" frame of reference (hey, it's not the real world!). A Vectorise geometry is one which has an invertible transformation into a list of Vector .
It occurred to me that Local could be an instance of Functor as follows:
instance Functor Local where
fmap f geom = localise (frame geom) (f $ local geom)
but the compiler complains that there is no instance of Vectorisable for the use of localise in the definition. Is there any way around this limitation using one of the myriad GHC extensions?
EDIT: As requested in the comments, here are some of the types used
local :: Local a -> a
frame :: Local a -> ReferenceFrame
localise :: (Vectorise a) => ReferenceFrame -> a -> Local a
The error is
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'
Which makes sense, because the type for fmap is (a -> b) -> fa -> fb . It can infer that a must be an instance of Vectorise , but I was wondering how it could infer that b was, unless I could specify (somehow) I could tell the compiler that f must have the restricted return type without defining another typeclass when there is already one that almost fits the bill already (or alternately, if someone could helpfully explain why restricting classes in this way would break type inference somehow).
ps. I also fixed up a typo where I had reversed local and frame reversed in the definition of fmap
The problem is that localise requires its second argument to have type Vectorise a => a , but when you apply f (which has type a -> b ) to the result of local (of type Vectorise a => a ), there is no guarantee that the resulting value will have type that is an instance of Vectorise . What you really want is a an analog of Functor that works only on types that have a Vectorise constraint.
Until recently, it wasn't possible to define such type classes. This is a well-known problem and the reason why Data.Set has no Functor or Monad instance. However, with the recent ConstraintKinds GHC extension such "restricted functors" finally became possible:
{-# 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)
You can read more about ConstraintKinds here and here.
上一篇: Rust和Haskell中的类型类的特性有什么区别？
下一篇: 类型类和GADT