Где блекджек, где мои шлюхи? Ничерта не работает! Войти !bnw Сегодня Клубы
Привет, TbI — HRWKA! 1239.0 пользователей не могут ошибаться!
?6944
прекрасное6443
говно5905
говнорашка5512
хуита4716
anime3066
linux2652
music2635
bnw2602
рашка2565
log2355
ололо2178
дунч1832
pic1815
сталирасты1491
украина1439
быдло1437
bnw_ppl1420
дыбр1238
гімно1158

Короче, вышел Type driven developement with Idris
Есть СКИДОС на 15$: ``ctwbastacon17'' , то есть чистые байтики можно купить за всего-лишь 25 баксов.

#KFOOF5 (2) / @ninesigns / 2825 дней назад

Написал двухстрочник isSorted (одна строчка — тип, вторая — значение (реализация функции))
@
не затайпчекался

#FJ13ZU (1) / @ulidtko / 3811 дней назад

бля прикол

% cat << EOF > hello.idr
heredoc> main : IO ()
heredoc> main = putStrLn "Hello world"
heredoc> EOF

% idris hello.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.11.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ./hello.idr
*hello> :compile hello.native
*hello> :js hello.js
*hello> 
Bye bye

% ./hello.native 
Hello world

% ls -l hello*
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:15 hello*
-rw-rw-r-- 1 ulidtko ulidtko  240 чер 19 02:17 hello.ibc
-rw-rw-r-- 1 ulidtko ulidtko   43 чер 19 02:17 hello.idr
-rw-rw-r-- 1 ulidtko ulidtko  36K чер 19 02:18 hello.js
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:18 hello.native*

110K
36K

-- на самом деле будущее.

#C9UUDK (8+2) / @ulidtko / 3825 дней назад

3.9 so
The so data type is a predicate on Bool which guarantees that the value is true:

data so : Bool -> Type where
    oh : so True

This is most useful for providing a static guarantee that a dynamic check has been made. For example, we
might provide a safe interface to a function which draws a pixel on a graphical display as follows, where
so (inBounds x y) guarantees that the point (x,y) is within the bounds of a 640 × 480 window:

inBounds : Int -> Int -> Bool
inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
drawPoint x y p = unsafeDrawPoint x y

ле к

#IDKL52 (4) / @ulidtko / 3825 дней назад
ipv6 ready BnW для ведрофона BnW на Реформале Викивач Котятки

Цоперайт © 2010-2016 @stiletto.