Typeclasses e GADT

Question

Sto assemblando una libreria di geometrie in haskell. Non ho intenzione di rilasciarlo, è solo un progetto che sto usando per migliorare la mia conoscenza della lingua.

Ho un tipo di dati Local, con la seguente definizione

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

Un frame di riferimento è un vettore indicando l'origine del telaio ed un angolo che rappresenta la rotazione del telaio, sia wrt definito il "assoluto "schema di riferimento (hey, non è il mondo reale!). Una geometria Vectorise è una che ha una trasformazione invertibile in una lista di Vector.

mi venne in mente che locale potrebbe essere un esempio di Functor come segue:

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

ma il compilatore si lamenta che non v'è alcuna istanza di Vectorisable per l'uso di localizzare nella definizione. C'è qualche modo per aggirare questa limitazione usando una delle innumerevoli estensioni GHC?

EDIT: Come richiesto nei commenti, qui sono alcuni dei tipi utilizzati

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

L'errore è

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' 

che ha un senso, perché il tipo di fmap è (a -> b) -> f a -> f b. Si può dedurre che a deve essere un'istanza di Vectorise, ma mi chiedevo come potesse dedurre che b fosse, a meno che non potessi specificare (in qualche modo) potrei dire al compilatore che f deve avere il tipo di restrizione limitato senza definire un altro typeclass quando è già uno che quasi si adatta già al disegno di legge (o in alternativa, se qualcuno potrebbe utilmente spiegare perché limitando le classi in questo modo si romperebbe l'inferenza di tipo in qualche modo).

ps. Ho anche sistemato un errore di battitura in cui avevo invertito local e frame invertiti nella definizione di fmap

Answer 1

Il problema è che localise richiede il suo secondo argomento di avere tipo Vectorise a => a, ma quando si applica f (che ha digitare a -> b) al risultato di local (di tipo Vectorise a => a), non è possibile garantire che il valore risultante abbia un tipo che è un'istanza di Vectorise. Quello che vuoi veramente è un analogo di Functor che funziona solo su tipi che hanno un vincolo Vectorise.

Fino a poco tempo fa, non era possibile definire tali classi di tipi. Questo è un problema ben noto e il motivo per cui Data.Set non ha l'istanza Functor o Monad. Tuttavia, con i recenti ConstraintKinds estensione GHC tali "funtori ristrette" divenne finalmente possibile:

{-# 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) 

Si può leggere di più su ConstraintKindshere e here.