/ / Perché non è possibile eseguire lo schema di corrispondenza su un tipo di famiglia? - haskell, tipi

Perché non riesco a riprodurre il modello su una famiglia di tipi? - haskell, tipi

Considera il seguente codice:

{-# LANGUAGE TypeFamilies #-}

data Twothings a b = Twothings a b

type family Leftthing a where
Leftthing (Twothings a b) = Leftthing a
Leftthing a = a

leftthing :: a -> Leftthing a
leftthing (Twothings a b) = leftthing a
leftthing b = b

Non viene compilato, con il seguente errore:

Couldn"t match expected type ‘a’
with actual type ‘Twothings a0 t0’
‘a’ is a rigid type variable bound by
the type signature for:
leftthing :: forall a. a -> Leftthing a

Si lamenta della linea leftthing (Twothings a b) = leftthing a. Se ho capito bene, non può unificare la variabile di tipo a nella firma del tipo con il tipo del costruttore Twothings. Ok, questo sembra avere un senso. Ma allora, come posso mai definire una funzione con famiglie di tipi nella firma del tipo?

risposte:

11 per risposta № 1

Quando dichiari

leftthing :: a -> Leftthing a

stai dicendo che il visitatore di leftthing arriva a scegliere cosa a è.

Quando poi scrivi

leftthing (Twothings a b) = leftthing a

sei presumendo che hanno scelto a Twothings digita, e poiché non è necessariamente il caso, il tuo programma viene rifiutato.

Potresti aver pensato che lo eri testare se loro avevano scelto a Twothings scrivi, ma no! Le informazioni sul tipo vengono cancellate prima del tempo di esecuzione, quindi non c'è modo di effettuare tale test.

tu può provare a ripristinare le informazioni necessarie sul tempo di esecuzione. Prima fammi correggere l'inconsistenza tra il tuo Leftthing e leftthing.

type family Leftthing a where
Leftthing (Twothings a b) = Leftthing{-you forgot the recursion!-} a
Leftthing a = a

Ora possiamo definire il GADT dei testimoni a Twothingness.

data IsItTwothings :: * -> * where
YesItIs   :: IsItTwothings a -> IsItTwothings (Twothings a b)
NoItIsn"t :: Leftthing a ~ a => IsItTwothings a
-- ^^^^^^^^^^^^^^^ this constraint will hold for any type
-- which is *definitely not* a Twothings type

E poi possiamo passare il testimone come argomento:

leftthing :: IsItTwothings a -> a -> Leftthing a
leftthing (YesItIs r) (Twothings a b) = leftthing r a
leftthing NoItIsn"t   b               = b

In effetti, il testimone è la codifica unaria del numero di left-nested Twothingses alla radice del tuo tipo. Sono sufficienti informazioni per determinare in fase di esecuzione la quantità corretta di disimballaggio da eseguire.

> leftthing (YesItIs (YesItIs NoItIsn"t)) (Twothings (Twothings True 11) (Twothings "strange" [42]))
True

Per riassumere, non è possibile trovare un tipo per modellocorrispondenza su un valore. Piuttosto, è necessario conoscere il tipo per eseguire la corrispondenza del modello (poiché il tipo determina il layout della memoria e non ci sono tag di tipo run time). Non è possibile eseguire la corrispondenza del modello sui tipi direttamente (perché non sono solo lì per essere abbinati). È possibile costruire tipi di dati che fungono da prova del tempo di esecuzione della struttura del tipo e corrispondono invece a quelli.

Forse, un giorno, il tuo programma funzionerà se gli dai il tipo

leftthing :: pi a. a -> Leftthing a

dove pi è il quantificatore dipendente, che indica che l'argomento del tipo nascosto non viene cancellato, ma piuttosto passato e abbinato in fase di esecuzione. Quel giorno non è ancora arrivato, ma penso che lo farà.