Qual è il tipo di (1 2) in Haskell?

Question

Stavo giocando in giro con abbracci e oggi è rimasto bloccato a una domanda molto semplice:

λ 1 1 
:: (Num a, Num (a -> t)) => t 

cosa sarebbe quel tipo è? Sto avendo problemi a leggere questo.

E se ha un tipo, perché? Direi che l'espressione 1 1 non è corretta e quindi il controllo dei tipi ha esito negativo, che è supportato dal compilatore Haskell.

Answer 1

No, non è mal-formata. Il tipo è strano e probabilmente non ci possono essere valori significativi per i quali ha senso ma è ancora permesso.

Ricordare che i valori letterali sono sovraccarichi. 1 è non un numero intero. È tutto del tipo Num. Le funzioni sono non escluse da questo. Non esiste una regola che dica a -> tnon può essere "un numero" (ad esempio un'istanza di Num).

Per esempio si potrebbe avere un instance dichiarazione del tipo:

instance Num a => Num (a -> b) where 
    fromInteger x = undefined 
    [...] 

ora 1 1 sarebbe semplicemente uguale undefined. Non molto utile ma ancora valido.

È possibile avere le definizioni utili di Num per le funzioni. Ad esempio, dal wiki

instance Num b => Num (a -> b) where 
    negate  = fmap negate 
     (+)   = liftA2 (+) 
     (*)   = liftA2 (*) 
     fromInteger = pure . fromInteger 
     abs   = fmap abs 
     signum  = fmap signum 

Con questo si può scrivere cose come:

f + g 

dove f e g sono funzioni numeri di ritorno.

L'utilizzo della suddetta dichiarazione di istanza 1 2 equivale a 1. Fondamentalmente un valore letterale utilizzato come funzione con l'istanza di sopra è uguale a const <that-literal>.

Answer 2

In Haskell, 1 non ha un tipo fisso. È "qualsiasi tipo numerico". Più esattamente, qualsiasi tipo che implementa la classe Num.

In particolare, è tecnicamente valido per un tipo di funzione come istanza di Num. Nessuno lo farebbe mai, ma tecnicamente è possibile.

Quindi il compilatore assume che il primo 1 è una sorta di tipo funzione numerica, e poi la seconda 1 è un qualsiasi altro tipo di numero (forse dello stesso tipo, forse uno diverso). Se cambiamo l'espressione, per esempio, 3 6, allora il compilatore sta assumendo

3 :: Num (x -> y) => x -> y 
6 :: Num x => x 
3 6 :: (Num (x -> y), Num x) => y