jfdm

class Tree():
    pass

class Node(Tree):
    def __init__(self,l,r,value):
        self.l = l
        self.r = r
        self.value = value

class Leaf(Tree):

jfdm

module DijkstraMonad

data NormalMonad : (A : Type) -> Type where
  Return : (value : a) -> NormalMonad a
  Bind : (doThis : NormalMonad a) -> (thenThis : a -> NormalMonad b) -> NormalMonad b

data DijkstraMonad : (A : Type) -> (NormalMonad A) -> Type where
  DReturn : {A : Type}
         -> (a : A)
         -> DijkstraMonad A (Return a)

jfdm

protocol Show {
    func show() -> String
}

class Tree<T> : Show {
    func show() -> String { return "" }
}

class Leaf<T> : Tree<T> {
    override func show() -> String {

jfdm

#!/usr/bin/env stack
-- stack --resolver lts-7.10 --install-ghc runghc
--  --package text
--  --package bytestring
--  --package containers
--  --package cassava
--  --package generics
--  --package vector
{-# LANGUAGE DeriveGeneric #-}
-- |

jfdm

-- ------------------------------------------------------------- [ Channel.idr ]
-- Module    : Channel.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
--
-- A effectful API for `System.Concurrency.Sessions`.
--
-- The code was partially adapted from existing code developed by
-- Edwin Brady (see `FILE_IO` effect) and Simon Fowler---see `Process`
-- effect in `IdrisNet2`.

jfdm

module Pairing

||| Model different group types.
data GTy = G1 | G2 | GT

||| Group element, implementation is incomplete but shows how dependent types can be used to provide more infomation.
data Element : GTy -> Type where
  MkElement : value -> (ty : GT) -> Element ty

||| Pairing information, implementation is incomplete.

jfdm

module Data.List.Constraints

import Data.Vect

data NotElem : a -> List a -> Type where
  NotHere  : NotElem x []
  NotThere : Eq ty => {x,y : ty}  -> {auto prf : x /= y = True} -> NotElem x xs -> NotElem x (y::xs)


data AllDiff : List a -> Type where

jfdm

module Data.DList

using (aTy : Type, elemTy : (aTy -> Type), x : aTy)

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export

jfdm

class Expr(object):
    def __init__(self):
        raise NotImplementedError
    def eval(self):
        raise NotImplementedError

class Value(Expr):
    def __init__(self, value):
        self.value = value

jfdm

||| You need latest version of my containers package:
|||     https://github.com/jfdm/idris-containers/
module Interp

import Data.DList
import Data.DeBruijn


data Ty = TyInt | TyBool | TyFun Ty Ty