Validierung auf Typenebene

Question

Angenommen, ich möchte Subtypen, die bestimmte Invarianten erfüllen, ohne Hilfe externer Tools wie LiquidHaskell konstruieren (idealerweise möchte ich dies auch ohne Typklassen tun). Was ist der eleganteste Weg, es zu tun? Bisher habe ich versucht, die folgenden:

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 

Ich gehe davon aus, dass, wenn ich nicht exportieren „Name“ Konstruktor aus dem Modul, ich werde eine funktionierende Lösung, weil der einzige Weg, ein Element des Typs zu konstruieren wäre durch makeValidated Funktion.

jedoch beklagt Compiler als solche:

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 

Wie kann ich das Problem beheben?

Answer 1

Underlying ist eine Art Funktion, die möglicherweise nicht injektiv ist. Das heißt:

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

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

Betrachten wir nun

validate (42 :: Int) 

Was soll das? Sollte es den Code A oder B aufrufen? Seit Underlying T1 = Underlying T2 = Int ist es unmöglich zu sagen.

Es ist unmöglich, validate eindeutig aufzurufen. Um dies zu vermeiden, ist eine mögliche Lösung ist ein „Proxy“ Parameter auf Ihre Validierungsfunktion hinzuzufügen:

data Proxy a = Proxy 

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

Jetzt können Sie verwenden:

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

Answer 2

Die validate-Funktion, wie geschrieben, ist in aktuellen GHC nicht verwendbar. Mit Blick auf seine Art Signatur:

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

könnte man vernünftigerweise denken, dass, da ein Wert vom Typ Underlying a, ein herausfinden können, welche Validated Instanz, nämlich zu verwenden, die a ein. Aber das ist ein Fehler: Da nicht injektiv ist, kann es Typen geben b und c für die Underlying b ~ Underlying c; daher kann weder b noch c eine kanonische Auswahl für die zu verwendende Instanz sein. Das heißt, ist keine gute Zuordnung F auf Typen, für die F (Underlying a) ~ a ist immer wahr!

Eine Alternative wäre die Verwendung einer Datenfamilie anstelle einer Typfamilie.

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

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