Typeclasses and GADTs

Question

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) -> f a -> f b. 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

Please show us the types of localise, local and frame and the error message that you get. My guess is that you're missing instance Vectorise for Local. — Mikhail Glushenkov
Done. I tried adding the instance declaration but it didn't help. It's the return type of f that I need to declare as Vectorise as far as I can see, not Local a. — ovangle

Mikhail Glushenkov Mikhail Glushenkov · Accepted Answer · 2013-04-04T12:53:32

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.

Typeclasses and GADTs

1 Answers