Earn extra honor and gain new allies!
Honor is earned for each new codewarrior who joins.
Learn more
Stats
Kata
Collections
Kumite
Social
Discourse
Published
donaldsebleung

Idris: Partial functions by default?

Just confirming that Idris does not enforce totality by default.

module PartialFunction

%access export

-- Partial function (implicit)
add : Int -> Int -> Int
add 3 5 = 8
donaldsebleung

Idris: Subverting the totality checker

It seems possible to subvert the totality checker by using assert_total on a partial function to convince Idris that it is total. This would place Idris theorem-proving Kata in jeopardy.

module TotalitySubversion

%access export
%default total

partial
add' : Int -> Int -> Int
add' 3 5 = 8

add : Int -> Int -> Int
add = assert_total add'
donaldsebleungFailed Tests

Idris: Total functions should not be able to make use of partial functions

Expected result - compilation error.

module Example

%access export
%default partial

add : Int -> Int -> Int
add 3 5 = 8
donaldsebleung

PureScript State Monad on Codewars?

Just testing whether the State monad in PureScript is available on Codewars.

module StateTest (factorialWithState) where

import Prelude

import Control.Monad.State (State, evalState, get, put)
import Data.Tuple (Tuple(..))

factorialWithState :: Int -> Int
factorialWithState n = evalState executionLoop (Tuple n 1)
  where
    executionLoop :: State (Tuple Int Int) Int
    executionLoop = do
      Tuple counter result <- get
      if counter == 0
        then pure result
        else do
          put (Tuple (counter - 1) (result * counter))
          executionLoop
donaldsebleungvs. donaldsebleung

PureScript Data.Ratio on Codewars?

As of 09/02/2019, Data.Ratio from purescript-rationals is available on Codewars.

donaldsebleungvs. donaldsebleungFailed Tests

Data.BigInt in PureScript?

purescript-bigints has been added to Codewars but now it seems there is a runtime JavaScript error due to missing modules on the JavaScript end :(

Code
Diff
  • module BigIntExample where

-- purescript-bigints now available on Codewars
-- but fails with runtime JavaScript error due to
-- missing JavaScript module

import Prelude

import Data.BigInt (BigInt, fromString)
import Data.Maybe (fromJust)
import Partial.Unsafe (unsafePartial)

biiiig :: BigInt
biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"
  • 11 module BigIntExample where
    22
    3+-- purescript-bigints now available on Codewars
    4+-- but fails with runtime JavaScript error due to
    5+-- missing JavaScript module
    6+
    33 import Prelude
    44
    55 import Data.BigInt (BigInt, fromString)
    66 import Data.Maybe (fromJust)
    77 import Partial.Unsafe (unsafePartial)
    88
    99 biiiig :: BigInt
    1010 biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"
donaldsebleungFailed Tests

PureScript Data.Leibniz on Codewars?

A simple test on whether Data.Leibniz is available as a PureScript module on Codewars.

module LeibnizExample where

import Data.Leibniz

reflexivity :: forall a. a ~ a
reflexivity = id
donaldsebleungFailed Tests

PureScript Data.Ratio on Codewars?

Just a test to see whether Data.Ratio for PureScript is available on Codewars. See test output for results.

module RatioExample where

import Prelude

import Data.Ratio

myRatio :: Ratio Int
myRatio = 3 % 10 -- 3 to 10, or 0.3
donaldsebleungFailed Tests

Data.BigInt in PureScript?

Just testing whether arbitrary-precision integers in PureScript are supported on Codewars. See the tests for the results.

module BigIntExample where

import Prelude

import Data.BigInt (BigInt, fromString)
import Data.Maybe (fromJust)
import Partial.Unsafe (unsafePartial)

biiiig :: BigInt
biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"
donaldsebleung

Welcome PureScript

PureScript is a strongly, statically typed functional programming language that compiles to and is easily interoperable with JavaScript. Its syntax and semantics are heavily influenced by Haskell so Haskell enthusiasts should find it easy to pick up PureScript.

Please don't forget to help PureScript leave Beta on Codewars and support the Codewars PureScript community by completing, authoring and translating more PureScript Kata. - @donaldsebleung

module WelcomePureScript (welcomeMsg) where

welcomeMsg :: String
welcomeMsg = "Welcome, PureScript!"
donaldsebleung

The Middle Schooler's Mistake

Theoretical Computer Science
Mathematics
Algorithms
Numbers

It is not uncommon to see a middle schooler incorrectly simplify the expression (a + b)^2 to a^2 + b^2 in his/her algebra assignments. While the two expressions may be equivalent for particular values of a and b (e.g. (0 + 0)^2 = 0^2 = 0 + 0^2 = 0^2 + 0^2), it is not true in general. So, how can we convince said middle-schooler that (a + b)^2 is not equal to a^2 + b^2 in general? This is equivalent to saying:

-- N.B. The domain of a, b is the natural numbers for
-- sake of simplicity
exists a b. (a + b)^2 /= a^2 + b^2

The general method for proving statements involving existential quantifiers is to provide a specific value or set of values such that the statement to be proven holds true - such value(s) are called witnesses. So, for example, we could provide the witnesses a = 1 and b = 1 in our case which reduces the statement to:

(1 + 1)^2 /= 1^2 + 1^2

And, of course, evaluating both sides of our equation gives 4 /= 2 which trivially holds.

Unfortunately, there is no direct way to encode existential quantifiers (and inequality) as a Haskell type. So what we could do is transform our original statement using known logical equivalences. The first thing to notice is that a /= b is defined as not (a = b) for any a, b:

exists a b. not ((a + b)^2 = a^2 + b^2)

Then, de Morgan's law for quantifiers tells us that exists a. not b is logically equivalent to not (forall a. b) for any b (which may or may not be related to a). Finally, to prove that not (forall a. b), it suffices to prove that asserting forall a. b leads to a contradiction (Void in Haskell). So our final type (minus a bit of required Haskell boilerplate code) is:

(forall a b. (a + b)^2 = a^2 + b^2) -> Void

See the code provided for the exact type signature of our proof and additional clarifications/explanations.

{-# LANGUAGE
  KindSignatures,
  GADTs,
  TypeOperators,
  TypeFamilies,
  UndecidableInstances,
  RankNTypes,
  EmptyCase #-}

module TheMiddleSchoolersMistake where

-- Void - the type representing contradictions in Haskell
import Data.Void

-- Peano's axioms for the natural numbers
data Z
data S n

data Natural :: * -> * where
  NumZ :: Natural Z
  NumS :: Natural n -> Natural (S n)

-- Axiom of reflexivity of equality: The very notion
-- of equality itself mandates that everything be
-- considered equal to itself
data (:=:) :: * -> * -> * where
  Refl :: a -> a :=: a

-- Peano addition, multiplication and exponentation
type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: n = n
type instance S n :+: m = S (n :+: m)

type family (:*:) (n :: *) (m :: *) :: *
type instance Z :*: n = Z
type instance S n :*: m = m :+: (n :*: m)

type family (:^:) (n :: *) (m :: *) :: *
type instance n :^: Z = S Z
type instance n :^: S m = n :*: (n :^: m)

-- Useful type synonyms for readability
type N1 = S Z -- The natural number 1
type N2 = S N1 -- The natural number 2
type N4 = N2 :+: N2 -- The natural number 4

-- Our proof that (a + b)^2 /= a^2 + b^2 in general
proof ::
  (forall n m.
    Natural n ->
    Natural m ->
    ((n :+: m) :^: N2) :=: ((n :^: N2) :+: (m :^: N2))) -> Void
proof mistake = let
  -- 1 is a natural number
  one :: Natural N1
  one = NumS NumZ
  -- To disprove (a + b)^2 = a^2 + b^2, we provide witnesses
  -- a = 1, b = 1 to our counterexample.  A witness is a
  -- value demonstrating the correctness of a logical statement
  -- involving existential quantifiers
  -- N.B. The witnesses could be anything else as long as it
  -- proves our point.  For example, we could've chosen a = 2,
  -- b = 3 instead and show that (2 + 3)^2 = 5^2 = 25 /= 13 =
  -- 2^2 + 3^2
  erroneous :: N4 :=: N2
  erroneous = mistake one one in
    -- Now we consider all possible cases where 4 = 2 and
    -- describe how to construct a proof of Void in each case
    -- However, there are no constructors that would allow us
    -- to construct a value of such a type!  The only possible
    -- constructor we could consider is Refl, but Refl always
    -- constructs values of a :=: a, never a :=: b where a and
    -- b are distinct types.  Therefore, we have already
    -- considered all (0) possible cases of 4 = 2 and we are
    -- done here.
    case erroneous of {}
donaldsebleung

Knights On A Chessboard

Theoretical Computer Science
Mathematics
Algorithms
Numbers

In international chess, a knight is a chess piece which can move in an L-shape (possibly mirrored) of size 2x1 in any orientation. Due to its unique movement patterns, it is the only chess piece able to "jump" past chess pieces of any color that may be blocking its way.

However, what is more interesting is that its movement patterns allow it to move to any desired square on a given chessboard provided that no same-color chess piece is occupying that desired square. This Haskell program seeks to prove this statement, extending the chessboard to an infinite chessboard (in the rightwards and upwards directions) characterized by an ordered tuple of natural numbers.

{-# LANGUAGE KindSignatures, GADTs #-}

module KnightsOnAChessboard where

-- Peano's axioms for the natural numbers
data Z
data S n

-- Definition of natural numbers (to prevent nonsensical types like `S Bool`)
data Natural :: * -> * where
  NumZ :: Natural Z
  NumS :: Natural n -> Natural (S n)

-- Legal moves of a knight in international chess
data KnightCanReach :: * -> * where
  NoMoves :: KnightCanReach (Z, Z)
  MoveRL :: KnightCanReach (n, m) -> KnightCanReach (S (S n), S m)
  MoveRR :: KnightCanReach (n, S m) -> KnightCanReach (S (S n), m)
  MoveUL :: KnightCanReach (S n, m) -> KnightCanReach (n, S (S m))
  MoveUR :: KnightCanReach (n, m) -> KnightCanReach (S n, S (S m))
  MoveLL :: KnightCanReach (S (S n), S m) -> KnightCanReach (n, m)
  MoveLR :: KnightCanReach (S (S n), m) -> KnightCanReach (n, S m)
  MoveDL :: KnightCanReach (n, S (S m)) -> KnightCanReach (S n, m)
  MoveDR :: KnightCanReach (S n, S (S m)) -> KnightCanReach (n, m)

-- Proof that knight can reach any square on a chessboard starting from (0, 0)
knightCanMoveAnywhere :: Natural n -> Natural m -> KnightCanReach (n, m)
knightCanMoveAnywhere NumZ NumZ = NoMoves
knightCanMoveAnywhere NumZ (NumS n) =
  MoveDR $ MoveUL $ MoveRL $ knightCanMoveAnywhere NumZ n
knightCanMoveAnywhere (NumS n) m =
  MoveLL $ MoveRR $ MoveUR $ knightCanMoveAnywhere n m
donaldsebleungFailed Tests

Cheating through internal stack?

Just testing whether it is possible to "cheat" using the stack internally maintained by the computer to "implement" stack operations (between calls) in NASM.

Conclusion: It doesn't seem to be possible - at least with the way I did it, I got a segfault during the first call to stack_push() which just attempts to push its second argument to the internal stack and returns to the caller, let alone the pop and peek operations. There also doesn't seem to be a reliable way to check whether the internal stack is empty. Thus, it should be safe to translate my recent Stacks kata into NASM.

global stack_push, stack_pop, stack_peek ; , stack_is_empty
section .text
stack_push:
  push rsi
  ret
stack_pop:
  pop rsi
  ret
stack_peek:
  pop rsi
  push rsi
  ret
donaldsebleung

Can one stack make a queue?

Yes and no. A queue can be implemented using one explicit stack by leveraging the technique of recursion in the "dequeue" operation but note that recursion is handled internally by a function call stack; hence, technically, there are still two stacks at work ;)

class Queue {
  constructor() {
    this._stack = []; // We will be using this array as a stack - only
    // its push and pop operations will ever be called
  }
  enqueue(data) {
    this._stack.push(data);
  }
  dequeue() {
    if (this._stack.length === 1)
      return this._stack.pop();
    else {
      var tmp = this._stack.pop(), result = this.dequeue();
      this.enqueue(tmp);
      return result;
    }
  }
}
donaldsebleungvs. donaldsebleung

Map/Dictionary/Associative Array as a binary search tree of entries

Data Structures
Algorithms
Binary Search Trees
Trees
Binary
Maps

Map/Dictionary/Associative Array as a binary search tree of entries

Suggested reading: Binary Search Tree - Wikipedia

Last time we saw how the map/dictionary/assoc array datatype can be implemented as a linked list of entries. We also noted how this implementation is seldomly used in real-world applications due to its sheer inefficiency for pretty much every operation.

So is there a way to make this data type more efficient? As it turns out, using a different data structure can really make an impact on the runtime complexity of operations on maps. One particular data structure that suits maps pretty well is the binary search tree (BST). A binary search tree is a special case of a binary tree where when one traverses its elements pre-order (left -> value -> right), the sequence of elements are in order. When the BST is perfectly balanced (i.e. all its branches have the same depth), its insertion, lookup and deletion operations are all logarithmic in time (O(log n)) because for every level you advance through the tree, you can effectively discard half of the tree. Another advantage of using a BST in our map is that we can implement a function converting the map into an iterator (if we wish to iterate through our key-value pairs in the map) such that the sequence of elements in the iterator are guaranteed to arrive in-order. However, the major drawback of (ordinary) BSTs is that if the elements are inserted in-order (or in reversed order), it degenerates into a linked list so its operations become O(n) again. Furthermore, if one inserts elements randomly into a BST, its operations converge towards an O(sqrt n) time complexity which is significantly less efficient than O(log n).

If only there were a way to ensure that our BST is sufficiently balanced at all times ... ;)

Code
Diff
  • #include <stddef.h>

typedef struct {
  // Denotes a key-value pair of integers, e.g. 7 => 34
  int key, value;
} Entry;

typedef struct node_t {
  // A node of a binary (search) tree - the internal implementation of our map
  Entry *entry;
  struct node_t *left, *right;
} Node;

typedef struct {
  // Our map datatype, implemented as a simple wrapper around our BST
  // This allows us to insert elements to a map by object reference and
  // reserves NULL for indicating an invalid reference to a Map (instead
  // of an empty map)
  Node *root;
} Map;

int map_get(const Map *map, int key) {
  // Retrieves the corresponding value for a given key in a map
  // Assumption: The given key-value pair in the map exists
  const Node *nd = map->root;
  while (nd->entry->key != key)
    nd = key < nd->entry->key ? nd->left : nd->right;
  return nd->entry->value;
}

void map_set(Map *map, int key, int value) {
  // Adds the key-value pair to the map if no entry with the given key exists;
  // otherwise modifies the value of the entry with the given key to the given value
  if (map->root == NULL) {
    map->root = malloc(sizeof(Node));
    map->root->entry = malloc(sizeof(Entry));
    map->root->entry->key = key;
    map->root->entry->value = value;
    map->root->left = map->root->right = NULL;
  } else {
    Node *nd = map->root;
    while (nd->entry->key != key) {
      const Node *tmp = key < nd->entry->key ? nd->left : nd->right;
      if (tmp == NULL)
        break;
      nd = tmp;
    }
    if (nd->entry->key == key)
      nd->entry->value = value;
    else if (key < nd->entry->key) {
      nd->left = malloc(sizeof(Node));
      nd->left->entry = malloc(sizeof(Entry));
      nd->left->entry->key = key;
      nd->left->entry->value = value;
      nd->left->left = nd->left->right = NULL;
    } else {
      nd->right = malloc(sizeof(Node));
      nd->right->entry = malloc(sizeof(Entry));
      nd->right->entry->key = key;
      nd->right->entry->value = value;
      nd->right->left = nd->right->right = NULL;
    }
  }
}

void map_remove(Map *map, int key) {
  // Removes the key-value entry from the map with the given key
  // Assumption: The key-value pair in the map exists
  if (map->root->entry->key == key) {
    if (map->root->right == NULL) {
      Node *tmp = map->root->left;
      free(map->root->entry);
      free(map->root);
      map->root = tmp;
    } else if (map->root->left == NULL) {
      Node *tmp = map->root->right;
      free(map->root->entry);
      free(map->root);
      map->root = tmp;
    } else if (rand() % 2) {
      Node *parent = map->root, *child = parent->left;
      while (child->right != NULL) {
        parent = child;
        child = child->right;
      }
      if (parent->left == child)
        parent->left = child->left;
      else
        parent->right = child->left;
      map->root->entry->key = child->entry->key;
      map->root->entry->value = child->entry->value;
      free(child->entry);
      free(child);
    } else {
      Node *parent = map->root, *child = parent->right;
      while (child->left != NULL) {
        parent = child;
        child = child->left;
      }
      if (parent->left == child)
        parent->left = child->right;
      else
        parent->right = child->right;
      map->root->entry->key = child->entry->key;
      map->root->entry->value = child->entry->value;
      free(child->entry);
      free(child);
    }
  } else {
    Node *nd_parent = map->root, *nd = key < nd_parent->entry->key ? nd_parent->left : nd_parent->right;
    while (nd->entry->key != key) {
      nd_parent = nd;
      nd = key < nd->entry->key ? nd->left : nd->right;
    }
    if (nd->right == NULL) {
      if (nd_parent->left == nd)
        nd_parent->left = nd->left;
      else
        nd_parent->right = nd->left;
      free(nd->entry);
      free(nd);
    } else if (nd->left == NULL) {
      if (nd_parent->left == nd)
        nd_parent->left = nd->right;
      else
        nd_parent->right = nd->right;
      free(nd->entry);
      free(nd);
    } else if (rand() % 2) {
      Node *parent = nd, *child = parent->left;
      while (child->right != NULL) {
        parent = child;
        child = child->right;
      }
      if (parent->left == child)
        parent->left = child->left;
      else
        parent->right = child->left;
      nd->entry->key = child->entry->key;
      nd->entry->value = child->entry->value;
      free(child->entry);
      free(child);
    } else {
      Node *parent = nd, *child = parent->right;
      while (child->left != NULL) {
        parent = child;
        child = child->left;
      }
      if (parent->left == child)
        parent->left = child->right;
      else
        parent->right = child->right;
      nd->entry->key = child->entry->key;
      nd->entry->value = child->entry->value;
      free(child->entry);
      free(child);
    }
  }
}
  • 11 #include <stddef.h>
    22
    33 typedef struct {
    4- // A key-value pair of integers
    4+ // Denotes a key-value pair of integers, e.g. 7 => 34
    55 int key, value;
    66 } Entry;
    77
    88 typedef struct node_t {
    9- // A node in a linked list - internal implementation of a Map
    10- Entry *entry; // The current entry in our map
    11- struct node_t *next; // The rest of our map
    9+ // A node of a binary (search) tree - the internal implementation of our map
    10+ Entry *entry;
    11+ struct node_t *left, *right;
    1212 } Node;
    1313
    1414 typedef struct {
    15- // Outer map wrapper (to hide interal implementation and
    16- // reserve `NULL` for representing an invalid map reference instead of an empty map)
    15+ // Our map datatype, implemented as a simple wrapper around our BST
    16+ // This allows us to insert elements to a map by object reference and
    17+ // reserves NULL for indicating an invalid reference to a Map (instead
    18+ // of an empty map)
    1717 Node *root;
    1818 } Map;
    1919
    2020 int map_get(const Map *map, int key) {
    21- // Returns the corresponding value to the key in the map
    22- // Assumption: the key is present in the map
    23- // (querying a nonexistent key yields undefined behavior)
    24- const Node *n = map->root;
    25- while (n->entry->key != key)
    26- n = n->next;
    27- return n->entry->value;
    23+ // Retrieves the corresponding value for a given key in a map
    24+ // Assumption: The given key-value pair in the map exists
    25+ const Node *nd = map->root;
    26+ while (nd->entry->key != key)
    27+ nd = key < nd->entry->key ? nd->left : nd->right;
    28+ return nd->entry->value;
    2828 }
    2929
    3030 void map_set(Map *map, int key, int value) {
    31- // Adds the key-value pair to the map if not present;
    32- // otherwise reassigns it at the corresponding entry
    33- Node *n = map->root;
    34- while (n != NULL && n->entry->key != key)
    35- n = n->next;
    36- if (n != NULL)
    37- n->entry->value = value;
    38- else {
    39- Node *tmp = map->root;
    32+ // Adds the key-value pair to the map if no entry with the given key exists;
    33+ // otherwise modifies the value of the entry with the given key to the given value
    34+ if (map->root == NULL) {
    4040 map->root = malloc(sizeof(Node));
    4141 map->root->entry = malloc(sizeof(Entry));
    4242 map->root->entry->key = key;
    4343 map->root->entry->value = value;
    44- map->root->next = tmp;
    39+ map->root->left = map->root->right = NULL;
    40+ } else {
    41+ Node *nd = map->root;
    42+ while (nd->entry->key != key) {
    43+ const Node *tmp = key < nd->entry->key ? nd->left : nd->right;
    44+ if (tmp == NULL)
    45+ break;
    46+ nd = tmp;
    47+ }
    48+ if (nd->entry->key == key)
    49+ nd->entry->value = value;
    50+ else if (key < nd->entry->key) {
    51+ nd->left = malloc(sizeof(Node));
    52+ nd->left->entry = malloc(sizeof(Entry));
    53+ nd->left->entry->key = key;
    54+ nd->left->entry->value = value;
    55+ nd->left->left = nd->left->right = NULL;
    56+ } else {
    57+ nd->right = malloc(sizeof(Node));
    58+ nd->right->entry = malloc(sizeof(Entry));
    59+ nd->right->entry->key = key;
    60+ nd->right->entry->value = value;
    61+ nd->right->left = nd->right->right = NULL;
    62+ }
    4545 }
    4646 }
    4747
    4848 void map_remove(Map *map, int key) {
    49- // Removes an entry from the map with the given key
    50- // Assumption: The given key-value pair exists
    51- // (attempting to delete a nonexistent entry yields undefined behavior)
    52- // This also implies that the map cannot be empty
    67+ // Removes the key-value entry from the map with the given key
    68+ // Assumption: The key-value pair in the map exists
    5353 if (map->root->entry->key == key) {
    54- Node *tmp = map->root->next;
    55- free(map->root->entry);
    56- free(map->root);
    57- map->root = tmp;
    70+ if (map->root->right == NULL) {
    71+ Node *tmp = map->root->left;
    5858 } else {
    59- Node *parent = map->root, *child = parent->next;
    60- while (child->next != NULL && child->entry->key != key) {
    61- parent = child;
    62- child = child->next;
    6363 }
    64- parent->next = child->next;
    65- free(child->entry);
    66- free(child);
    6767 }
    6868 }
Loading more items...