Timers and GADT

Question

I am building a geometry library in haskell. I'm not going to release it, it's just a project that I use to improve my language skills.

I have a Local data type with the following definition

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

The reference frame is a vector indicating the beginning of the frame and the angle representing the rotation of the frame, both are determined by the "absolute" reference system (hey, this is not a real world!). A Vectorise geometry is one that has a reversible conversion to a Vector list.

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 to use localization in the definition. Is there a way around this limitation using one of the many 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 

Error

 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' 

This makes sense because the type for fmap is (a -> b) -> fa -> fb . He may conclude that a should be an instance of Vectorise , but I was wondering how it could conclude that b was, if I could not specify (somehow), I could tell the compiler that f should have a limited return type without defining another type if there is already one that already almost matches the count (or, alternatively, if someone can explain why class constraints in this way can somehow violate type inference).

ps. I also set a typo in which I changed the value of Local and frame in the fmap definition

Answer 1

The problem is that localise requires the second argument to be of type Vectorise a => a , but when you apply f (which is of type a -> b ) to a local result (of type Vectorise a => a ), there is no guarantee that the resulting value will be of the type that is an instance of Vectorise . What you really want is an analog of Functor , which only works for types with a Vectorise constraint.

Until recently, it was not possible to define these types of classes. This is a well-known problem and the reason Data.Set does not have an instance of Functor or Monad . However, with the recent ConstraintKinds GHC extension, such "limited functors" have finally become 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 fa :: Constraint type SubCats fa = () rfmap :: (SubCats fa, SubCats fb) => (a -> b) -> fa -> fb instance RFunctor Local where type SubCats Local a = Vectorise a rfmap f geom = localise (frame geom) (f $ local geom) 

Read more about ConstraintKinds here and here .