Suppose we have a functional language where objects don't have explicitly defined types, but where named properties can nonetheless be accessed on objects. Is it then possible for the compiler to trace throughout the program which properties could be accessed on which variables and do full type inference on the program so that if the program compiles, it's guaranteed that all accessed properties must exist? For example, each property name could correspond to a Haskell typeclass and the compiler could check the soundness using Hindley-Milner.
Sì, possiamo fare qualcosa di simile! Ma dubito che sarebbe pratico.
Diamo un'occhiata a come potrebbe essere. Considera la seguente funzione ordinaria di Python (tratta dal link ):
def test_sequential_pop():
model = Sequential()
model.add(Dense(num_hidden, input_dim=input_dim))
model.add(Dense(num_class))
model.compile(loss='mse', optimizer='sgd')
x = np.random.random((batch_size, input_dim))
y = np.random.random((batch_size, num_class))
model.fit(x, y, epochs=1)
model.pop()
assert len(model.layers) == 1
assert model.output_shape == (None, num_hidden)
model.compile(loss='mse', optimizer='sgd')
y = np.random.random((batch_size, num_hidden))
model.fit(x, y, epochs=1)
Supponiamo di voler eseguire la digitazione anatra e vogliamo anche l'inferenza di tipo. Python non ha inferenza di tipo, ovviamente, ma Haskell lo fa, e possiamo convincere Haskell a fare qualcosa di simile alla digitazione anatra.
Digitare anatra significa che non ci interessa davvero i tipi reali di tutte le cose che stiamo usando; tutto ciò che ci interessa è che le cose possano essere usate insieme, nel modo in cui le usiamo. Per rendere felice Haskell, utilizzeremo parametri impliciti per creare oggetti e accedere alle loro proprietà. Proprio come vogliamo, il compilatore traccerà a quali proprietà si accede su quali variabili e così via.
Il nostro codice Haskell potrebbe essere simile a questo:
testSequentialPop = do
model <- ?newSequential
?newDense numHidden (Just inputDim) >>= ?addLayer model
?newDense numClass Nothing >>= ?addLayer model
?compileModel model "mse" "sgd"
x <- ?getRandom [batchSize, inputDim]
y <- ?getRandom [batchSize, numClass]
?fitModel model x y 1
?popModel model
?assert (?length (?layers model) == 1)
?assert (?outputShape model == [Nothing, Just numHidden])
?compileModel model "mse" "sgd"
y2 <- ?getRandom [batchSize, numHidden]
?fitModel model x y 1
Finora, tutto bene. Questo codice verrà compilato bene. Se scriviamo il resto del programma, funzionerà anche bene.
Quindi qual è il problema? Chiediamo a GHC quale sia il tipo di testSequentialPop . GHC dice:
testSequentialPop
:: (Eq a5, Eq a7, Monad m, Num a2, Num a3, Num a5, Num a7, Num t2,
Num a9, ?addLayer::t -> a1 -> m a, ?assert::Bool -> m a6,
?compileModel::t -> [Char] -> [Char] -> m a8,
?fitModel::t -> t1 -> t1 -> a9 -> m b, ?getRandom::[t2] -> m t1,
?layers::t -> t3, ?length::t3 -> a5,
?newDense::a2 -> Maybe a3 -> m a1, ?newSequential::m t,
?outputShape::t -> [Maybe a7], ?popModel::t -> m a4) =>
m b
Ooh, è piuttosto complicato.
Il problema qui è che la funzione deve menzionare ogni operazione che esegue sugli oggetti di input. Se disponi di un programma di grandi dimensioni che fa cose complicate con gli oggetti di input, potresti ritrovarti con un tipo che contiene centinaia, forse migliaia di vincoli.
L'inferenza di tipo aiuterà cose un piccolo , ma non così tanto. L'inferenza di tipo a volte salva i programmatori dal dover calcolare i tipi stessi o dal doverli scrivere per intero. I programmatori dovranno ancora capire i tipi per capire come possono essere utilizzate le funzioni e per diagnosticare cosa causa errori di tipo.
Detto questo, ci sono strumenti che fanno qualcosa di simile a questo. Ad esempio, Checkmarx crea uno strumento di analisi del codice statico in grado di rilevare alcune vulnerabilità della sicurezza, come gli attacchi di SQL injection, tracciando il modo in cui gli oggetti vengono creati e utilizzati. Un attacco di SQL injection è essenzialmente un errore di digitazione anatra: si sta creando un oggetto (una stringa contenente l'input dell'utente) e quindi si esegue un'operazione (utilizzandola come query SQL) su di esso, anche se quell'oggetto non supporta quell'operazione . Checkmarx traccia l'intero percorso di questo oggetto, dalla creazione all'utilizzo, e, se trova qualche problema, mostra l'intero percorso.
Non so se sarebbe possibile estendere questa idea in modo che funzioni su tutte , piuttosto che su operazioni che rappresentano un pericolo per la sicurezza.