La corrispondenza del modello sulle funzioni a livello di tipo è possibile, ma non sul livello di valore, perché questa differenza?

Question

In this carta da SPJ, a pagina 3 e 4, è scritto:

class Mutation m where 
    type Ref m :: * -> * 
    newRef :: a -> m (Ref m a) 
    readRef :: Ref m a -> m a 
    writeRef :: Ref m a -> a -> m() 

instance Mutation IO where 
    type Ref IO = IORef 
    newRef = newIORef 
    readRef = readIORef 
    writeRef = writeIORef 

instance Mutation (ST s) where 
    type Ref (ST s) = STRef s 
    newRef = newSTRef 
    readRef = readSTRef 
    writeRef = writeSTRef 

e:

La dichiarazione della classe introduce ora una funzione di tipo Ref (con un tipo specificato ) a fianco le solite funzioni di valore come newRef (ognuna con un tipo specificato). Analogamente, ogni dichiarazione di istanza contribuisce con una clausola che definisce la funzione di tipo sul tipo di istanza insieme a un testimone per ogni funzione di valore.

Diciamo che Ref è una famiglia di tipo o un tipo associato della classe Mutation. Si comporta come una funzione al livello di tipo, quindi chiamiamo anche una funzione di tipo Ref. L'applicazione di una funzione di tipo utilizza la stessa sintassi dell'applicazione di un costruttore di tipo : Rif m a sopra significa applicare la funzione di tipo Rif a m, quindi applicare il costruttore di tipi risultante a a.

Quindi, in altre parole,

Ref :: (*->*)->*->*

cioè Ref prende una funzione livello tipo come argomento, come Maybe o IO o [] e produce un'altra funzione livello di tipo, ad esempio IORef usando una corrispondenza di modello , vale a dire Ref è definito da una corrispondenza di modello .

Quindi, come è possibile che sia possibile associare la corrispondenza alle funzioni a livello di tipo ma non a livello di valore?

Ad esempio,

fun2int:: (Int->Int)->Int 
fun2int (+)=2 
fun2int (*)=3 

non è possibile scrivere perché uguaglianza funzioni è undecidable.

1) Quindi, come è possibile che a livello di tipo questo non causi problemi?

2) È perché le funzioni a livello di tipo sono di tipo molto limitato? Quindi nessun tipo di funzione a livello di tipo può essere un argomento per Ref, solo alcuni selezionati, vale a dire quelli dichiarati dal programmatore e non funzioni come (+), che sono più generali di quelli dichiarati dal programmatore? È questo il motivo per cui la corrispondenza del modello di funzione di livello del tipo non causa alcun problema?

3) La risposta a questa domanda è relativa alla parte this delle specifiche GHC?

Answer 1

In poche parole, non v'è alcun pattern matching sulla funzione del tipo livello valori, ma solo sulla loro nome.

In Haskell, come in molte altre lingue, i tipi vengono tenuti separati dal nome, anche se la loro rappresentazione è identica.

data A x = A Int x 
data B x = B Int x 

Sopra, A e B sono due differenti costruttori di tipo, anche se descrivono la stessa funzione del tipo di livello: in pseudo-codice \x -> (Int, x), grossolanamente. In un certo senso, queste due identiche funzioni a livello di tipo hanno un nome/identità diversa.

Questo è diverso da

type C x = (Int, x) 
type D x = (Int, x) 

che descrivono entrambi la stessa funzione del tipo livello come sopra, ma non introducono due nuovi nomi dei tipi. Quanto sopra sono solo sinonimi: denotano una funzione, ma non hanno una propria identità distinta.

Questo è il motivo si può aggiungere un'istanza di classe per A x o B x, ma non per C x o D x: tentare di fare quest'ultima dovrebbe aggiungere un'istanza al tipo (Int, x) invece, relativi l'istanza ai nomi dei tipi (,), Int anziché.

A livello di valore, la situazione non è molto diversa. In effetti, abbiamo costruttori di valori, che sono funzioni speciali con un nome/identità e funzioni regolari senza un'identità reale. Siamo in grado di pattern match contro un modello, costruita da costruttori, ma non contro qualsiasi altra cosa

case expOfTypeA of A n t -> ... -- ok 
case someFunction of succ -> ... -- no 

Nota che a livello di tipo non possiamo fare pattern matching così facilmente. Haskell consente di fare lo sfruttamento solo delle classi di tipi. Ciò viene fatto per preservare alcune proprietà teoriche (parametricity) e per consentire anche un'efficiente implementazione (permettendo la cancellazione del tipo - non è necessario taggare ogni valore con il suo tipo in fase di runtime). Queste funzionalità hanno il prezzo di limitare la corrispondenza del modello di livello di tipo alle classi di tipi: ciò pone un certo onere per il programmatore, ma i vantaggi superano gli svantaggi.

Answer 2

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} 
import GHC.TypeLits 

Riportiamo alcuni paralleli tra il tipo e il livello di valore in Haskell.

Primo, abbiamo funzioni illimitate sia per tipo che per livello di valore. A livello di testo, puoi esprimere quasi tutto usando famiglie di tipi. È impossibile la corrispondenza del modello su funzioni arbitrarie su entrambi i tipi o livello di valore. Per esempio. non si può dire

type family F (a :: *) :: * 
type family IsF (f :: * -> *) :: Bool where 
    IsF F = True 
    IsF notF = False 

-- Illegal type synonym family application in instance: F 
-- In the equations for closed type family ‘IsF’ 
-- In the type family declaration for ‘IsF’ 

dati secondo luogo, abbiamo pienamente applicati e costruttori di tipo, come ad esempio Just 5 :: Maybe Integer a livello valore o Just 5 :: Maybe Nat sul piano tipo.

È possibile pattern matching su questi:

isJust5 :: Maybe Integer -> Bool 
isJust5 (Just 5) = True 
isJust5 _ = False 

type family IsJust5 (x :: Maybe Nat) :: Bool where 
    IsJust5 (Just 5) = True 
    IsJust5 x = False 

Nota la differenza tra le funzioni arbitrarie e tipo/dati costruttori. La proprietà dei costruttori è talvolta chiamata generatività. Per due diverse funzioni f e g, è molto probabile che sia f x = g x per alcuni x. D'altra parte, per i costruttori, f x = g x implica f = g.Questa differenza rende indecidibile il primo caso (pattern-matching su funzioni arbitrarie) e il secondo caso (pattern-matching su costruttori completamente applicati) decidibile e trattabile.

Finora abbiamo visto la coerenza tra il tipo e il livello di valore.

Infine, abbiamo parzialmente applicato (compresi i costruttori non applicati). A livello di testo, questi includono Maybe, IO e [] (non applicato), nonché Either String e (,) Int (parzialmente applicato). A livello di valore, non abbiamo applicato Just e Left e parzialmente applicato (,) 5 e (:) True.

La condizione di generatività non interessa se l'applicazione è piena o meno; quindi non c'è nulla che precluda la corrispondenza dei modelli per i costruttori parzialmente applicati. Questo è ciò che vedi a livello di testo; e noi potrebbe averlo anche a livello di valore.

type family IsLeft (x :: k -> k1) :: Bool where 
    IsLeft Left = True 
    IsLeft x = False 

isLeft :: (a -> Either a b) -> Bool 
isLeft Left = True 
isLeft _ = False 
-- Constructor ‘Left’ should have 1 argument, but has been given none 
-- In the pattern: Left 
-- In an equation for ‘isLeft’: isLeft Left = True 

Il motivo per cui non è supportato è l'efficienza. I calcoli a livello di tipo vengono eseguiti durante la compilazione in modalità interpretata; quindi possiamo permetterci di portare a un sacco di metadati sui tipi e le funzioni di tipo per la corrispondenza dello schema su .

I calcoli sul livello del valore sono compilati e devono essere veloci quanto possibile. Mantenere un numero sufficiente di metadati per supportare la corrispondenza dei modelli su costruttori applicati parzialmente complicherebbe il compilatore e rallenterebbe il programma al runtime ; è semplicemente troppo per pagare una caratteristica così esotica.