Сопоставление с образцом предполагаемого типа

Почему приведенный ниже тип не проверяется? Тип _ выводится как Double.

{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}

module Main (main) where

data D a = D a

main =
  let
    n = D (1 :: forall a. (Floating a) => a)
  in
    case n of
      D (_ :: forall a. (Floating a) => a) -> return ()

haskell pattern-matching higher-rank-types
person denormal    schedule 02.01.2017    source источник
comment
Haskell не поддерживает такие типы, как D (forall a. (Floating a) => a), который, похоже, вам нужен здесь для n, потому что это потребовало бы непредикативного полиморфизма. В то время как 1 здесь действительно полиморфен, D 1 по-прежнему имеет значение по умолчанию D Double из-за правил определения типов по умолчанию в Haskell (в противном случае тип будет считаться неоднозначным).   -  person Alexis King    schedule 02.01.2017

Ответы (1)


arrow_upward
4
arrow_downward

Похоже, тип, который вы ожидаете для n, — это D (forall a. (Floating a) => a), но это категорически не тип, который выводится. На самом деле, если вы попытаетесь добавить аннотацию этого типа к n, вы обнаружите, что GHC будет громко жаловаться. Такой тип потребует от GHC поддержки непредикативного полиморфизма, чего в настоящее время нет (дополнительную информацию о том, что это такое и почему это сложно, см. в Что такое предикативность?).

Тип, который фактически выводится для n, это D Double. На самом деле это результат двух действующих факторов: ужасного ограничения мономорфизма и типа Haskell невыполнение правил. Из-за ограничения мономорфизма n следует рассматривать как мономорфный тип (поскольку синтаксически он не является функцией и не имеет явной аннотации типа). По этой причине D 1 будет неоднозначным, поскольку 1 :: forall a. (Floating a) => a полиморфен. Однако в этом случае в Haskell есть правила по умолчанию для числовых типов, в основном для того, чтобы избежать необходимости разрешать неоднозначности из-за полиморфных числовых литералов Haskell.

Поскольку вы явно добавили аннотацию типа к 1, чтобы сделать его Floating, то Haskell применяет правило по умолчанию для типов с плавающей запятой и по умолчанию Double. Следовательно, тип n подразумевается как D Double.

Если вы отключите ограничение мономорфизма, то тип n будет немного более интересным типом forall a. Floating a => D a, но это будет более простой универсальный квантифицированный тип, а не экзистенциально квантифицированный тип, который вам нужен.

person Alexis King    schedule 02.01.2017