Convalida a livello di tipo

Question

Dire che mi piacerebbe costruire sottotipi che soddisfano determinati invarianti senza l'aiuto di strumenti esterni come LiquidHaskell (idealmente voglio farlo anche senza typeclass). Qual è il modo più elegante per farlo? Finora ho provato quanto segue:

class Validated a where 
    type Underlying a 
    validate :: Underlying a -> Bool 
    construct :: Underlying a -> a 
    use :: a -> Underlying a 

makeValidated :: Validated a => Underlying a -> Maybe a 
makeValidated u = if validate u 
        then Just (construct u) 
        else Nothing 


newtype Name = Name String 
instance Validated Name where 
    type Underlying Name = String 
    validate str = and [ isUppercase (str !! 0) 
         , all isLetter str ] 
    construct = Name 
    use (Name str) = str 

suppongo che se non esportare il costruttore "Nome" dal modulo, avrò una soluzione di lavoro, perché l'unico modo per costruire un elemento di tipo sarebbe attraverso la funzione makeValidated.

Tuttavia compilatore si lamenta in quanto tale:

Could not deduce (Underlying a0 ~ Underlying a) 
from the context (Validated a) 
    bound by the type signature for 
      makeValidated :: Validated a => Underlying a -> Maybe a 
    at validated.hs:11:18-55 
NB: `Underlying' is a type function, and may not be injective 
The type variable `a0' is ambiguous 
Possible fix: add a type signature that fixes these type variable(s) 
In the first argument of `validate', namely `u' 
In the expression: validate u 
In the expression: 
    if validate u then Just (construct u) else Nothing 

Come posso risolvere il problema?

Answer 1

Underlying è una funzione di tipo, che potrebbe non essere iniettiva. Cioè:

instance Validate T1 where 
    type Underlying T1 = Int 
    validate = ... -- code A 

instance Validate T2 where 
    type Underlying T2 = Int 
    validate = ... -- code B 

consideri ora

validate (42 :: Int) 

Cosa dovrebbe fare questo? Dovrebbe chiamare il codice A o B? Dal Underlying T1 = Underlying T2 = Int, è impossibile dirlo.

Impossibile chiamare validate senza ambiguità. Per evitare questo, una possibile soluzione è quella di aggiungere un parametro "proxy" alla funzione di validazione:

data Proxy a = Proxy 

class Validate a where 
    validate :: Proxy a -> Underlying a -> Bool 

Ora è possibile utilizzare:

validate Proxy (42 :: Int)    -- still ambiguous! 
validate (Proxy :: Proxy T1) (42 :: Int) -- Now OK! 
validate (Proxy :: Proxy T2) (42 :: Int) -- Now OK! 

Answer 2

La funzione validate, come scritto, non è utilizzabile nel GHC corrente. Guardando la sua firma Tipo:

validate :: Validated a => Underlying a -> Bool 

si potrebbe ragionevolmente pensare che, dato un valore di tipo Underlying a, si può capire quale Validated esempio da utilizzare, vale a dire, il a uno. Ma questo è un errore: poiché Underlying non è iniettivo, potrebbero esserci tipi b e c per i quali Underlying b ~ Underlying c; quindi né b né c possono essere una scelta canonica per quale istanza utilizzare. Cioè, ci è nessuna buona mappatura F su tipi per cui F (Underlying a) ~ a è sempre vero!

Un'alternativa sarebbe utilizzare una famiglia di dati anziché una famiglia di tipi.

class Validated a where 
    data Underlying a 
    validate :: Underlying a -> Bool 

instance Validated Name where 
    data Underlying Name = Underlying String 
    validate (Underlying name) = ...