к
Яuby
Rиby
там много вариантов не попало в график
Rиby
там много вариантов не попало в график
x : List List Int
x = Debug.crash ""
Size: a a a
2017 November 01
NK
Кто знает, почему в Elm компилируется такое:
Kind check не производится. Issue даже есть.
NK
Типы они решили пока(?) не чинить, судя по всему.
MP
Но у List то всяко
* -> *, так что второй параметр точно лишнийЕсли для некоторыйх параметров для мервой звездочки, вторая сама станет * -> *, то тип может использоваться с разным количеством аргументов. Аналогично функции id.
MP
Ну функции id один аргумент. Но id (+) 2 4 вполне нормально работает. Возможно, и тип такой можно сконструировать (сходу из repl не смог, но возможность допускаю).
AP
id и always в Эльме подхаченные
AP
А в Хаскеле у них поликайндовый тип
NK
Ну функции id один аргумент. Но id (+) 2 4 вполне нормально работает. Возможно, и тип такой можно сконструировать (сходу из repl не смог, но возможность допускаю).
потому что id (+) = (+)?
MP
ID:351615646
потому что id (+) = (+)?
Ну да. С типами в Haskell такое не проходит, но в Idris сделать можно.
Idris> the (id List Int) [1,2,3]
[1, 2, 3] : List Int
Idris> the (id List Int) [1,2,3]
[1, 2, 3] : List Int
NK
почему не проходит? твой пример работает в хаскеле
NK
@potan ^
NK
у нас просто в типе
idₐ₀ : ∀ a₀ . a₀ → a₀ параметр a₀ становится a₀ = ∀ a₁ . a₁ → a₁ → a₁ и мы получаем idₐ₀ : ∀ a₁ . (a₁ → a₁ → a₁) → a₁ → a₁ → a₁2017 November 02
AP
В хаскеле просто реальный тип у
id посложнееAP
(->) a b, это просто тип с кайндом * -> * -> *, А у (+), тип (->) a ((->) a a), который вообще * -> *AP
Т.о. от
id требуется лишь уметь принимать k -> *, где k - любой кайнд. Это вполне кодируется на ХаскелеNK
(->) a b, это просто тип с кайндом * -> * -> *, А у (+), тип (->) a ((->) a a), который вообще * -> *у
(→) a b кайнд ★ → ★ → ★? серьезно?AP
Джва параметра у типа
(a -> b) - две звёздочки, третья - сам применённый типAq
так тут оба уже применены
NK
так тут оба уже применены
^