martinsson

module moneychange
import Data.String

--%default total
data Coin  : (value: Nat) -> Type where
  OneCent  : Coin 1
  FiveCent : Coin 5
  TenCent  : Coin 10

-- without this type that hides the value I can't put the coins in a list

martinsson

import Data.List

UserId: Type
UserId = String

data Message: (userId: UserId) -> Type where 
  MkMessage: (userId: UserId) -> String -> Message userId
data DeleteCommand: (userId: UserId) -> Type where
  MkDeleteCommand: (userId: UserId) -> DeleteCommand userId  

martinsson

import {Observable} from "rxjs/Observable";
import {Subject} from "rxjs/Subject";

export function fibonacciStream() {

  let fibN2: Subject<number> = new Subject();
  // initiate the series, so that both this and fibN1 has atleast one
  setImmediate(() => { 
    fibN2.next(0);
    fibN2.next(1);

martinsson

import * as _ from 'lodash'

function sumPreviousTwo(numbers: number[]) {
  let [n2, n1] = _.takeRight(numbers, 2);
  return n2 + n1;
}

export function fibonacci(length: number): number {
  let firstTwoNumbers = [0, 1];

martinsson

import {assert} from "chai";
import {Roman} from "../src/Roman";

function toRoman(arabic: number) {
  return new Roman().toRoman(arabic);
}

describe('RomanNumbers', () => {
  describe('toRoman() is', () => {

martinsson

import Data.So
%default total

fizz : Nat -> Bool
fizz n = (modNatNZ n 3 SIsNotZ) == 0

buzz : Nat -> Bool
buzz n = (modNatNZ n 5 SIsNotZ) == 0

data FizzT : (n: Nat) ->  Type where

martinsson

%default total

-- Proofs that a value is divisible my 3 and 5 respectively
IsFizz : (k : Nat) -> Type
IsFizz k = (modNatNZ k 3 SIsNotZ = 0)

IsBuzz : Nat -> Type
IsBuzz k = (modNatNZ k 5 SIsNotZ = 0)

-- The type Fizzbuzz, one can only construct an instance of Fizz if one can provide

martinsson

data Change : (amount: Nat) -> Type where
  NoChange : Change Z
  SucChange : (prev: Change amount) -> Change (S amount)
  Composite : (ch1: Change amount1) -> (ch2: Change amount2) ->
              {auto prf: amount1 + amount2 = amount'}-> Change amount'
--  Simple : (value: Nat) -> (quantity: Nat) ->
--           {auto prf: value * quantity = amount'} -> Change amount'


extractAmount : (Change amount) -> Nat

martinsson

-- diversion, money change, fizzbuzz (divisible by)

-- Learnings: 
-- Tom: I understand this, until(!) I implement it
--      functions that take a proof, ensure that they're never called without that proof and
--      the arguements to the proof
--      For instance constructors

martinsson

const { Maybe, Either } = require('monet');

class TripService {

    // Monadic version of the public function, returns an Either
    getTripsByUserEither(user, loggedUser) {
        return Maybe.fromNull(loggedUser)
            .toEither('User not logged in.')
            .flatMap(connectedUser => this._doGetTripsByUser(user, connectedUser));