инстанцировании Haskell типы параметрических данных

Question

Пытаясь понять Haskell type parameter ниже,

Prelude> data T a = C1 a | C2 (a -> a) 

Prelude> :t C1 1 
C1 1 :: Num a => T a 

Prelude> :t C1 (+1) 
C1 (+1) :: Num a => T (a -> a) 

Prelude> :t C2 1 
C2 1 :: Num (a -> a) => T a 

Prelude> :t C2 (+1) 
C2 (+1) :: Num a => T a 

К моему знанию C1 1 может быть и речи, C2 1 не имеет смысла, C1 (+1) и C2 (+1) кажутся противоречивыми.

Почему ни один из типовых чеков выше не жаловался? Ваше понимание очень ценится.

Answer 1

Если вы хотите, чтобы сообщение об ошибке, создать ситуацию, в которой a должна быть такой же, как:

> :t [C1 (+1), C2(+1)] 
Couldn't match expected type .... 

В вашем примере a s различны, как a1 и a2. И никаких ошибок

Answer 2

В Haskell, числовые литералы не полиморфный:

1 :: Int 
1 :: Integer 
1 :: Double 
... 

Технически это достигается с помощью общего типа

1 :: Num a => a 

Таким образом, "1 может быть любого типа, при условии, что такой тип относится к классу Num ».

Когда вы делаете, например, C2 1, 1 берется из типа функции a -> a, и дополнительное ограничение создается для того, чтобы a -> a является Num:

C2 1 :: Num (a -> a) => T a 

Конечно, функция является не число. Почему тогда нет ошибки типа? Потому что в Haskell не запрещено расширять класс Num, чтобы включить функции. Вы можете сделать это с, , например:

instance Num b => Num (a -> b) where 
    fromInteger n = \_ -> n 
    x + y = \z -> x z + y z 
    ... 

превращая 1 :: a -> a в функцию «константа один».

Это может дать такой код (надуманный пример следует)

case (some value of type T Int) of 
C1 x -> x 
C2 f -> (f + g) 50 
-- assumning g :: Int -> Int 
-- result is f 50 + g 50 

Если вы не предоставите экземпляр, то код не является по своей сути неправильно, так как экземпляр может быть добавлен позже. В этом случае ограничение будет зависеть в вашем коде, поскольку оно не может быть освобождено. Если вы попытаетесь преобразовать T a в любой тип, не включающий a, для этого необходимо выполнить ограничение Num, и в это время компилятор действительно будет жаловаться.

---

случаи, связанные с (+1) можно объяснить, заметив, что это раздел оператор, так что это не просто унарный плюс в передней части 1.В частности,

(+1) means \x -> x + 1 

так (+1) на самом деле функция последования.