[haskell] Inferred type is less polymorphic than expected

Так в этом же и весь смысл, что вся информация о типе теряется. Значение какого типа ты собираешься вытаскивать, если тип может быть практически любой? Вместо этого при конструировании в T сохраняется словарь класса Show, используемый при вызове методов этого класса.

Об этом написано даже в букваре пользователя ghc. http://www.haskell.org/ghc/docs/7.0.3/html/users_guide/data-type-extensions.h...

Что за словарь? Операционно в ghc конструкция «data T a = forall a. Show a => C a» делает в конструкторе C типа T два поля: одно с ссылкой на объект неизвестного типа a, а другое с ссылкой на Show-инстанс для этого типа.

> словарь

Show-инстанс

Его я и имел в виду.

Так в этом же и весь смысл, что вся информация о типе теряется.

Вопрос на самом деле в связи с вот этим - http://www.haskell.org/haskellwiki/Heterogenous_collections#Existential_types, т.е. мы можем значение любого типа (forall a. a) упаковать (pack) и тогда гомогенные структуры можно использовать как гетерогенные. Но хотелось бы иметь возможность делать unpack. У GHC это restriction как я понял. Кстати, на роль pack/unpack подойдут toDyn/fromDyn из Data.Dynamic, но в этом случае нужно всё время дописывать инстансы (делать deriving), а pack/unpack это тоже самое но автоматически на уровне системы типов.

Значение какого типа ты собираешься вытаскивать, если тип может быть практически любой?

Любого типа. Например, id имеет тип (forall a. a -> a), т.е. в данном случае «любой тип» выступает в роли возвращаемого значения. Т.е. это ограничение на определяемые типы данных, а не на «любой тип» в качестве значения вообще. Вот тут ещё есть на эту тему - http://okmij.org/ftp/Haskell/types.html#some-impredicativity

Можно сделать вот так:

{-# LANGUAGE ExistentialQuantification #-}

import Unsafe.Coerce

data Any = forall a. MkAny a

pack :: forall a. a -> Any
pack = MkAny

unpack :: forall a. Any -> a
unpack (MkAny x) = unsafeCoerce x

-- :t [pack 5, pack "5"]
-> [pack 5, pack "5"] :: [Any]

-- unpack $ pack 5 :: Int
-> 5

но это unsafe.

Не представляю, как такой unpack возможен на уровне типов. Кстати, тип у unpack неправильный, не

unpack :: forall a. Any -> a

unpack :: exists a. Any -> a

unpack :: Any -> (forall a. a -> b) -> b

> У GHC это restriction как я понял.

GHC тут не при чем, это обычная логика.

GHC тут не при чем, это обычная логика.

Что функция не может вернуть произвольное значение из универсума? Просто {A : Set} -> ... -> A, как в agda.

Кстати, тип у unpack неправильный

Ну не суть, там type schema - pack :: a -> Any, unpack :: Any -> b, в первом случае это соответствует forall, а во втором exists. Можно видеть, что для всех типов id = pack . unpack.

Не представляю, как такой unpack возможен на уровне типов

Вот если делать полиморфный (Any a), то с pack :: a -> Any a, unpack :: Any a -> a всё понятно. Почему не может быть обобщенного АТД Any, который скрывает этот полиморфизм - т.е. не мешает строить гетерогенные структуры (вроде [Any]), и оставляет тот же смысл у pack/unpack — pack :: a -> Any[a], unpack :: Any[a] -> a.

в UHC, если не ошибаюсь, такой синтаксис валиден

Ну он в haskell' есть, так что это будущий стандарт.

Ну вот возьмём такой код

module Main where

import Any (pack, unpack)

main :: IO ()
main = do
    let any = [pack 1, pack "hello"]
    print (map unpack any :: String)
    print (map unpack any :: Int)

Как он должен выполняться? Или как компилятор может увидеть проблему?

Имелись в виду [String] и [Int].

> Что функция не может вернуть произвольное значение из универсума?

Где ты в экзистенциональных типах нашел юниверсум?

s/экзистенциональных/экзистенциальных/

Если немножко дополнить предыдущуй код, а именно использовать безопасный cast из Data.Typeable, то получится более менее полное решение:

{-# LANGUAGE ExistentialQuantification #-}

module Any ( Any, pack, unpack ) where

import Data.Typeable ( Typeable, TypeRep, typeOf, cast )

data Any = forall a. Typeable a => MkAny a TypeRep

instance Typeable Any where
  typeOf (MkAny _ t) = t

pack :: Typeable a => a -> Any
pack a = MkAny a $ typeOf a

unpack :: Typeable a => a -> Any -> Maybe a
unpack _ (MkAny a t) = cast a

Правда это почти тоже что Data.Dynamic, с той разницей, что вместо примитива реализации (вроде Any в GHC) экзистенциальные типы.

Или как компилятор может увидеть проблему?

Можно делать выборки:

map (unpack 0) [pack 5, pack "5"]
> [Just 5,Nothing]

map (unpack "0") [pack 4, pack "5"]
> [Nothing,Just "5"]

Сделать map ((flip fromDyn) 5) [...] тоже ведь не получится.

Чтобы unpack работал вообще без задания типа или сэмпла (сэмпл, кстати, не используется как значение, он только позволяет зафиксировать тип) - это нужно иметь возможность делать (cast a t), где cast :: (Typeable a, Typeable b) => a -> TypeRep -> b (TypeRep представляет тип b).

Где ты в экзистенциональных типах нашел юниверсум?

Имеется в виду, что с помощью forall мы квантифицируем по универсуму (Set в agda). Например, id :: forall a. a -> a определён по всему универсуму.

с использованием дополнительной полиморфной функции.

data Any = forall a. Show a => MkAny a

pack :: Show a => a -> Any
pack = MkAny

unpack :: Any -> (forall a. Show a => a -> b) -> b
unpack (MkAny a) f = f a

unpack (pack 5) $ \x -> show x
> "5"

unpack (pack 5) id
> Inferred type is less polymorphic than expected

такая же ерунда :( Использовать в вычислениях можно, вытащить - нельзя.

Значит, инстансы всё же дописывать придётся.

Чтобы unpack работал вообще без задания типа или сэмпла…

…TypeRep представляет тип b

Тоже ведь своего рода задание типа?

Я бы ещё newtype добавил, что-то вроде такого:

newtype TypedAny a = { unTypedAny :: Maybe a }

unpack :: (Typeable a) => Any -> TypedAny a
unpack (MkAny a _) = cast a

Чуть больше кода упаковки-распаковки, зато никаких сэмплов вроде (undefined :: String) в коде. Не нравятся они мне.

такая же ерунда :( Использовать в вычислениях можно, вытащить - нельзя.

Именно так. Экзистенциальный тип задаёт минимальную степень полиморфизма, и функция должна быть достаточно полиморфной, чтобы принять значение любого типа. (\x -> show x) достаточно полиморфна, а в случае с id её первый аргумент унифицируется с мономорфным типом b. Разумеется, компилятор такое не пропустит.

В моём коде выше с newtyp'ом пара тривиальных неточностей, не будем обращать на них внимания :)

Имеется в виду, что с помощью forall мы квантифицируем по универсуму (Set в agda). Например, id :: forall a. a -> a определён по всему универсуму.

What has this to do with existential quantification? Simply that MkFoo has the (nearly) isomorphic type

 MkFoo :: (exists a . (a, a -> Bool)) -> Foo

Чего не ясно в слове «exists»?

А морфизм, морфизм-то есть?

Да-да-да, я тоже с радостью вспоминаю тот эпичный тред :)

Чего не ясно в слове «exists»?

Э... Так о чём мы говорим? :) У нас для *каждого* объекта в унивресуме должно выполняться id = pack . unpack (треугольничек такой). При pack forall-квантификация, при unpack - exists, и при этом они с друг другом связаны через id.

Э... Так о чём мы говорим? :)

Напомню, ты говоришь про это:

unpack :: forall a. Any -> a

Никакого exists здесь я здесь не вижу. Если хочешь честный unpack, то для

data T = forall a. Show a => T a

он будет таким

unpack :: T -> (forall a. Show a => (a -> r)) -> r
unpack (T x) f = f x

Никакого restriction, никаких unsafe. И agda тоже приплетать не стоит.

Или же средствами GHC (rank-2 types)

unpack :: Any -> (forall a. a -> b) -> b

, т. е. только с использованием дополнительной полиморфной функции.

Это то же, что и exists. Обычная трансляция одного квантора через другой ∃a. P(a) = ¬∀a. ¬P(a)