MK
А кстати, в реифайд же не экзистенциальные типы
Size: a a a
2020 November 10
MK
Что я вас с толку сбил
MK
Сорян
ЗП
Ну а как ещё?
обманул ты меня)
A newtype constructor cannot have existential type variables
A newtype constructor cannot have existential type variables
ЗП
newtype SomeType = forall x. SomeType Int
MK
Да я и сам себя обманул похоже
MK
Три раза
ЗП
но через сколема можно просунуть)
к
data X = forall a. Show a => X a
это пара из инстанса Show a и значения типа a
и это уже exist
newtype X = X (forall a. Show a => a)
это функция в ньютайпе от инстанса в значение, которая не хранит инстанс, а потребует инстанс для Show a, при использовании значения внутри, которого нет
это не exist
это пара из инстанса Show a и значения типа a
и это уже exist
newtype X = X (forall a. Show a => a)
это функция в ньютайпе от инстанса в значение, которая не хранит инстанс, а потребует инстанс для Show a, при использовании значения внутри, которого нет
это не exist
ЗП
но это уже элиминация exists через forall
ЗП
newtype X = X (forall r. (forall a. Show a => (a -> r) ) -> r)
YS
конечно нет, exist тип это минимум пара, если не учитывать тип, то из инстанса и значения
да, я тупанул
написал
написал
newtype F = F {unF :: forall a . a} х(ЗП
а это просто черч энкодинг пары
это и есть сколемизация
MK
У сколема спроси
ЗП
ну тут енкодинг exists