Dissertation • Publications • Sam Elliott • Developer & Researcher
A Concurrency System for Idris & Erlang My Bachelors Dissertation at the University of St Andrews • Supervisor: Dr Edwin Brady Abstract Concurrent programming is notoriously difficult, due to needing to reason not only about the sequential progress of any algorithms, but also about how information moves between concurrent agents. What if programmers were able to reason about their concurrent progr
Copatterns
Motivation So, what are copatterns, and why do we want them? Essentially, copatterns allow us to make projections on the left-hand side of function definitions. Left-hand side projections make sense for definitions from which we primarily want to extract data, contrary to injecting data into data constructors. Examples include record types and coinductive types. Observation vs. Construction Copatt
Tic Tac Type: Dependent Types with Idris
Functional programming provides a fundamental basis for reasoning about our programs and building out principled abstractions. However, it is not enoug…
IdrisでWebアプリを書く
2. 自己紹介 • 田中英行(@tanakh) • Haskellとかやってます • 「すごいHaskellたのしく学ぼう」翻訳 • 「Parallel and Concurrent Programming in Haskell」翻訳中 • Idris初心者 3. Idrisとは？ • http://www.idris-lang.org/ • “Fully Dependent Type” なプログラミング言語 • Cf. CoqとかAgdaとかATSとか • 純粋関数型 • 正格評価 • 様々な言語へのバックエンド • C言語 • LLVM • Java • JavaScript 4. 処理系のインストール • $ cabal install idris $ idris ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Versio
Try Idris
Idris is a language for practical, dependently typed, functional programming. The Idris Tutorial is the best resource for becoming familiar with with the language. You can use the REPL above to play around without installing the compiler on your computer. Give these examples a go: "Hello world" reverse (the (Vect 3 _) [1, 2, 3]) the (n ** Vect (S n) Int) (3 ** [1, 2, 3, 4]) You can also compile Id
Idris as a Library - BAM Weblog
I’ve been playing around with making a dependently typed language. It’s based upon Martin-Löf Type Theory (commonly just called Type Theory, TT). Turns out that implementing a dependent type system is a great way to learn how to use one! I had written code to translate from my toy languages’ terms into TT - but I wanted a compiler, so that I could execute it somewhere outside of the evaluator/norm
Differences between Agda and Idris
I'm starting to dive into dependently-typed programming and have found that the Agda and Idris languages are the closest to Haskell, so I started there. My question is: which are the main differences between them? Are the type systems equally expresive in both of them? It would be great to have a comprehensive comparative and a discussion about benefits. I've been able to spot some: Idris has type
Idris: A Language for Type-Driven Development
Idris: A Language for Type-Driven Development Idris is a programming language designed to encourage Type-Driven Development. In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
andyarvanitis - Overview
https://github.com/ajhager/IdrJS
GitHub - idris-hackers/iQuery: Idris Lib to interact with the DOM and Browser API for the JavaScript backend
Scala vs Idris: Dependent Types, Now and in the Future
Private Site
GitHub - edwinb/SDL-idris: SDL bindings package for idris
jhenahan/idris-vim · GitHub
Course on Programming with Idris: Videos/Slides | Idris