Можешь рекомендовать?

ну, мне нравится

Збс

збс книга

как жс туториал

я пока пытаюсь собрать в Idris2.  show' : Vect n a -> String ему не нравится, нужно show' : Vect m a -> String. Разбираюсь с can't match on S ?k (Erased argument)

Show a => Show (Vect n a) where
   show xs = "[" ++ show' xs ++ "]" where
       show' : Vect n a -> String
       show' Nil        = ""
       show' (x :: Nil) = show x
       show' (x :: xs)  = show x ++ ", " ++ show' xs    

Ну у меня так и вроде не ругается

но у меня первый

Угу, в нём show' : Vect n a ... шадовит n из Show (Vect n a), во втором - нет

То есть, чтобы выяснить, где вводится новая имплицитная переменная нужно читать доку или экспериментировать

сделай топ левел функцию

она ничего не будет шедоить

Это я уже решил. Достаточно использовать другое имя для имплицитной переменной в show'

ну или так

там же версия 0.2 или какая

понятно что не все работает как надо)

The problem in AI/ML and the concept of "AI winter" to me was always the barrier of the fact that we're just doing predictions, with no deep meaning or comprehension of features. The layman thinks there's magic, but there's not, so when that truth is revealed there will be problems. There's nothing intelligent about our Artificial Intelligence; we're just doing statistics with big data and added sprinkles. OpenAI just proved they could do statistics with even bigger data and more expensive sprinkles.

чувак на хакерньюсе идеально выразился что касается того, что меня напрягает в ML статус кво

OP https://news.ycombinator.com/item?id=23623845