Skip to content

Instantly share code, notes, and snippets.

View raichoo's full-sized avatar

raichoo raichoo

147 followers · 3 following
View GitHub Profile
@raichoo
raichoo / gist:5700522
Last active December 18, 2015 00:59
JavaScript Lib
module Main
{-
Compile with:
idris --package javascript --target javascript test.idr -o test.js
<html>
<head>
@raichoo
raichoo / gist:5709002
Last active November 4, 2022 21:21
Experiments with dependently typed JSON in Idris
module JSON
import Data.SortedMap
data JSONType: Type where
JSONArray : Vect JSONType n -> JSONType
JSONString : JSONType
JSONNumber : JSONType
JSONBool : JSONType
JSONObject : SortedMap String JSONType -> JSONType
@raichoo
raichoo / bezier.hs
Last active December 19, 2015 21:29
Idris version of https://github.com/hrldcpr/Bezier.hs/blob/master/Bezier.hs
module Bezier
Point : Type -> Nat -> Type
Point = Vect
-- parametric line between two points:
line : Num a => Point a d -> Point a d -> a -> Point a d
line p q t = zipWith interpolate p q
where interpolate a b = (1 - t)*a + t*b
@raichoo
raichoo / gist:6196942
Last active December 20, 2015 21:19
total
fold_length : List a -> Nat
fold_length = foldl (\n, _ => S n) Z
total
foldr_reduce : (n : Nat) -> (xs : List a) ->
let f : (Nat -> a -> Nat) = (\n, _ => S n) in
S (foldr (flip (.) . flip f) id xs n) = foldr (flip (.) . flip f) id xs (S n)
foldr_reduce n Nil = refl
foldr_reduce n (x :: xs) = let ih = foldr_reduce (S n) xs in
@raichoo
raichoo / gist:6556748
Created September 13, 2013 22:08
Positional arguments for the javascript FFI in Idris
module Main
FIO : FTy
FIO = FAny (IO ())
foo : String -> String -> IO ()
foo a b = putStrLn $ a ++ b
test : String -> (String -> String -> IO ()) -> IO ()
test s f =
@raichoo
raichoo / Vect.scala
Created October 1, 2013 16:31
Playing with dependent types in Scala
package Vect
import scala.language.higherKinds
sealed trait Nat
sealed trait Z extends Nat
sealed trait S[N <: Nat] extends Nat
trait Exists[A, +B[_ <: A]] {
type fst <: A
@raichoo
raichoo / gist:8686084
Created January 29, 2014 11:23
Ongoing "Idris to JavaScript" optimization work
/*
recTestHelper : Integer -> Integer -> Integer
recTestHelper n 0 = n
recTestHelper n m = recTestHelper (n * m) (m - 1)
*/
var __IDR__wnurecTesturecTestHelper0swnurecTesturecTestHelper0 = function(me0,me1){
var __var_2 = __IDRRT__EVALTC(me1)
if (__var_2.equals(__IDRRT__ZERO)) {
return me0;
@raichoo
raichoo / gist:8686168
Created January 29, 2014 11:30
boolElim translated into JavaScript
var __IDR__BoolPreludenuboolElim = function(me0,me1,me2,me3){
var __var_4 = __IDRRT__tailcall(function(){
return __IDR__mEVAL0(me1)
});
if (__var_4 instanceof __IDRRT__Con && 0 == __var_4.tag) {
return me3;
} else if (__var_4 instanceof __IDRRT__Con && 1 == __var_4.tag) {
return me2;
}
}
@raichoo
raichoo / gist:9214929
Created February 25, 2014 18:37
total
isElem' : DecEq a => (e : a) -> (t : Tree a) -> Dec (IsElem e t)
isElem' x Leaf = No $ \p => noElemInLeaf x p
where
total
noElemInLeaf : (x : a) -> IsElem x Leaf -> _|_
noElemInLeaf x Here impossible
isElem' x (Branch l y r) with (decEq x y)
isElem' x (Branch l x r) | Yes refl = Yes Here
@raichoo
raichoo / gist:9326998
Last active August 29, 2015 13:56
Hello world
var __IDRLT__APPLY65610 = function(mfn0,marg0){
return new __IDRRT__Cont(function(){
return __IDRRT__print(mfn0.vars[0])
})
}
var __IDRLT__APPLY65611 = function(mfn0,marg0){
return new __IDRRT__Cont(function(){
return __IDR__mAPPLY0(mfn0.vars[1],marg0)
})