ЗП
ну судя по тому что мне сейчас сказал зига, скелимизация это синоним черч-энкодингу, больше ничего сказано не было
не совсем, тут 2-ранг
∃x. P(x) = ¬∀x. ¬P(x)
Size: a a a
2020 November 10
ЗП
ЗП
¬ = forall r. rЗП
ну это как бы один из законов де Моргана, только для кванторов
к
а у черча будет не ранк-2?
data Instance c = c => Instance
newtype X =
X (forall r. (forall a. Instance (Show a) -> a -> r) -> r)
тут rank-2 возникает просто потому что полиморфное значение
абстрактный по типу нонемпти такой же будет
newtype NonEmpty' =
NonEmpty' (forall r. (forall a. [a] -> a -> r) -> r)
data Instance c = c => Instance
newtype X =
X (forall r. (forall a. Instance (Show a) -> a -> r) -> r)
тут rank-2 возникает просто потому что полиморфное значение
абстрактный по типу нонемпти такой же будет
newtype NonEmpty' =
NonEmpty' (forall r. (forall a. [a] -> a -> r) -> r)
ЗП
вообще Черч это не про кванторы)
все ошибочно Черча называют с кванторами, а по факту это Бом-Берардуччи
все ошибочно Черча называют с кванторами, а по факту это Бом-Берардуччи
ЗП
https://wiki2.org/en/Skolem_normal_form
а нормальная форма Сколема это как раз исключение exists и не важно как ты это сделаешь
а нормальная форма Сколема это как раз исключение exists и не важно как ты это сделаешь
ЗП
Every existentially quantified type of rank n+1 can be encoded as a universally quantified type of rank n
YS
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
вот это кажется понятно, спасибо!
ЗП
ЗП
JS
ах вот почему Foundation создали! чтобы скорее на Арм переехать, а то макинтоши новые уже испеклись, а Хаскеля на них нет
JS
хорошо, но недостаточно
MP
недавно читал (сходу не нашел, где-то на реддите), что так себе там все с армом
MP
Клапауций сказал бы наверное "вообще плохо, а с армом совсем плохо"
IK
хорошо, но недостаточно
А нельзя через llvm пускать просто?
JS
А нельзя через llvm пускать просто?
нельзя, ghc не отдаёт llvm как артефакт