Блог

Какова точная семантика ограничений равенства? Являются ли эти два типа точно эквивалентными?

 f :: Int -> IO [T]
g :: (a ~ T) => Int -> IO [a]
 

Является g ли мономорфная или полиморфная функция, которая работает только для T? Это тривиально кажется мономорфным, но будет ли компилятор обрабатывать это так f ? В разделе руководства пользователя GHC, посвященном ограничениям равенства, не обсуждаются детали реализации.

Кажется, я вспоминаю, что для полиморфных функций могут потребоваться ВСТРОЕННЫЕ или СПЕЦИАЛИЗИРОВАННЫЕ прагмы для включения всех оптимизаций, и может потребоваться время выполнения, чтобы сделать вещи излишне полиморфными. Может ли это быть g и здесь, или GHC узнает лучше и сразу упростит это? Или, может быть, это зависит?

Ну, типы, конечно, не совсем эквивалентны.

Средство проверки типов считает их разными типами. Если вы скомпилируете с -ddump-types помощью, вы увидите:

 TYPE SIGNATURES
  f :: Int -> IO [Double]
  g :: forall a. (a ~ Double) => Int -> IO [a]
 

Эти два типа также ведут себя по-разному во время компиляции. Например, с TypeApplications расширением, g @Double 10 является допустимым выражением, а f @Double 10 не является.

В core ограничение равенства реализовано — как и все ограничения — как дополнительный аргумент словаря, и вы увидите это различие в типах, отраженных в сгенерированном ядре. В частности, если вы скомпилируете следующую программу:

 {-# LANGUAGE GADTs #-}

module EqualityConstraints where

import Control.Monad

f :: Int -> IO [Double]
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
g n = replicateM n readLn
 

с:

 ghc -ddump-types -ddump-simpl -dsuppress-all -dsuppress-uniques 
    -fforce-recomp EqualityConstraints.hs
 

вы увидите ядро, подобное следующему:

 -- RHS size: {terms: 12, types: 22, coercions: 3, joins: 0/0}
g =  @ a $d~ eta ->
      case eq_sel $d~ of co { __DEFAULT ->
      replicateM
        $fApplicativeIO eta (readLn ($fReadDouble `cast` <Co:3>))
      }

-- RHS size: {terms: 6, types: 4, coercions: 0, joins: 0/0}
f =  n -> replicateM $fApplicativeIO n (readLn $fReadDouble)
 

и это различие будет сохраняться в ядре даже при -O2 .

Действительно, если вы предотвратите встраивание, результирующее конечное ядро (и даже конечный STG) потребует некоторой ненужной передачи словаря, как вы можете видеть, играя с:

 {-# LANGUAGE GADTs #-}

import Control.Monad

f :: Int -> IO [Double]
{-# NOINLINE f #-}
f n = replicateM n readLn

g :: (a ~ Double) => Int -> IO [a]
{-# NOINLINE g #-}
g n = replicateM n readLn

main = do
  f 2
  g 2
 

и компиляция с -ddump-simpl помощью и -ddump-stg .

Насколько я вижу, эта разница все еще видна даже в оптимизированной сборке с -O2 .

Итак, я думаю, можно с уверенностью сказать, что g это обрабатывается достаточно полиморфно, чтобы действительно применялись оговорки о затратах времени выполнения на ненужный полиморфизм.

Одно большое различие заключается в том, когда вы используете такие ограничения в классе типов.

 class F a where f :: Int -> IO [a]
instance F Int where f n = pure [1,2,3]
instance (a ~ Int) => F a where f n = pure [1,2,3]
 

Если вы используете объявление второго экземпляра, вы не сможете создавать какие-либо другие экземпляры, потому что, несмотря на ограничение, все типы будут объединяться с помощью a .