Первый шаг в решении, как мне кажется, состоит в том, чтобы прочувствовать, что аргумент и возвращаемое значение - один и тот же терм, который, однако, имеет два разных типа (иначе второе уравнение пройдет проверку). Ну а дальше думать, как заставить второе споткнуться на унификации, при том, что первое должно остаться устойчивым. Можно и без чистых фантомов решить, Either, например, подойдет.
ну да, ну да. Проблема с условием в том, что если попытаться выразить поточнее, получится почти ответ; а если так как есть, то не очень ясно, что именно нужно решить - тип функции :-)
Да, Either подойдет, но не пройдет проверку один из кейсов, и искомый вид имеет не вся функция, а лишь один кейс.
Comments 15
data T = T (IO ())
instance Eq T where { _ == _ = True }
f = id
Теперь:
id $ putStrLn "abc" == putStrLn "abc" -- не компилируется
id $ T (putStrLn "abc") == T (putStrLn "abc") -- компилируется
Reply
Reply
Reply
Reply
Reply
(полагаю, вы имели в виду "аргумент", а не "конструктор").
Reply
data T a = T Int
f :: T Int -> T String
f (T a) = T a
Reply
Reply
Reply
map f (x:xs) = f x: map f xs
map f xs = xs -- нельзя, т.к. xs не того типа
А в чистом виде - функтор Const.
data Const a b = Const a
type T = Const A
Reply
Reply
Да, Either подойдет, но не пройдет проверку один из кейсов, и искомый вид имеет не вся функция, а лишь один кейс.
Reply
Leave a comment