the
Haskell type system is very powerful compared to the industrial
programming languages; a nice demonstration of this is its ability to
represent and maintain the invariants of balanced search trees [AVL,
red-black]; and the Haskell code is not even longer [or much messier]
than the Agda version [Agda is a real dependently typed language, the
most popular one currently]
https://doisinkidney.com/posts/2018-07-30-verified-avl.html
https://doisinkidney.com/posts/2018-07-30-verified-avl.html
No comments:
Post a Comment