deniok: (ухмыляюсь)
[personal profile] deniok
Приведите пример таких объявлений типа данных с конструктором данных T и сигнатуры функции f, что реализация
f (T x) = T x
проходила бы проверку типов, a
f x = x
нет.

Date: 2016-04-07 09:57 am (UTC)
From: [identity profile] john kozlov (from livejournal.com)
В голову приходит только дебильное:

data T = T (IO ())
instance Eq T where { _ == _ = True }

f = id

Теперь:

id $ putStrLn "abc" == putStrLn "abc" -- не компилируется
id $ T (putStrLn "abc") == T (putStrLn "abc") -- компилируется

Date: 2016-04-07 10:44 am (UTC)
From: [identity profile] migmit.livejournal.com
Ну, простейший вариант это data T = T Int Int. Или имеется в виду что-то другое?

Date: 2016-04-07 10:45 am (UTC)
From: [identity profile] migmit.livejournal.com
Даже нет, простейший — это data T = T.

Date: 2016-04-07 10:52 am (UTC)
From: [identity profile] john kozlov (from livejournal.com)
T x не скомпилируется. У T должен быть хотя бы один конструктор.

Date: 2016-04-07 10:58 am (UTC)
From: [identity profile] migmit.livejournal.com
Так, вроде ж, и не должно?

(полагаю, вы имели в виду "аргумент", а не "конструктор").

Date: 2016-04-07 11:02 am (UTC)
From: [identity profile] migmit.livejournal.com
А, пардон. Не так понял задание.

Date: 2016-04-07 11:02 am (UTC)
From: [identity profile] migmit.livejournal.com
Спасибо, я не так понял задание.

Date: 2016-04-07 11:04 am (UTC)
From: [identity profile] deni-ok.livejournal.com
У тебя, вроде, выходит наоборот - второе тайпчекается, а первое нет.

Date: 2016-04-07 11:07 am (UTC)
From: [identity profile] migmit.livejournal.com
data T a = T Int
f :: T Int -> T String
f (T a) = T a

Date: 2016-04-07 11:22 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Ага, фантомы.

Date: 2016-04-07 12:36 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Хорошая задачка.

Date: 2016-04-07 02:10 pm (UTC)
From: [identity profile] john kozlov (from livejournal.com)
Короче, я неправильно понял задание. Я прочитал f x = x как f x == x и задача кардинально изменила свой смысл. Поэтому и написал instance Eq

Date: 2016-04-09 07:10 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
Вообще-то, из условия не очень понятно, что с такой ситуацией сталкивался. Как правило, ситуация возникает в каком-нибудь из кейсов - например:

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

Date: 2016-04-09 07:59 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Первый шаг в решении, как мне кажется, состоит в том, чтобы прочувствовать, что аргумент и возвращаемое значение - один и тот же терм, который, однако, имеет два разных типа (иначе второе уравнение пройдет проверку). Ну а дальше думать, как заставить второе споткнуться на унификации, при том, что первое должно остаться устойчивым. Можно и без чистых фантомов решить, Either, например, подойдет.

Date: 2016-04-09 08:36 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
ну да, ну да. Проблема с условием в том, что если попытаться выразить поточнее, получится почти ответ; а если так как есть, то не очень ясно, что именно нужно решить - тип функции :-)

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

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 9th, 2025 06:17 pm
Powered by Dreamwidth Studios