luochen1990

Coq Emacs (Spacemacs) Develop Environment Prepare Guide

main reference:

https://gist.github.com/mtrsk/10a03927490f9edb1f7a2cd72792b0ec

The Dependencies Graph

luochen1990

import GHC.Stack
import Data.Time.Clock

h0 :: Int -> Int
h0 x = if x == 3 then errorWithoutStackTrace "abuse h" else (x + 3) `div` (x - 3)

h1 :: Int -> Int
h1 x = if x == 3 then withFrozenCallStack . error $ "abuse h" else (x + 3) `div` (x - 3)

timeIt :: IO a -> IO a

luochen1990

use std::fmt;

enum List<A> {
    Nil,
    Cons(A, Box<List<A>>),
}

impl<A: fmt::Display> fmt::Display for List<A> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {

luochen1990

//c++11
#include<cstdio>
#include<string>
#include<iostream>

using namespace std;

template<typename A>
struct List {
    A label;

luochen1990

import GHC.Stack

foo :: [Int] -> Int
foo xs = last xs + 1

bar :: [Int] -> Int
bar xs = foo xs

xs :: [Int]
xs = []

luochen1990

{-# language InstanceSigs #-}

import GHC.Stack

class Next v where
    next :: HasCallStack => v -> v

instance Next Bool where
    next :: Bool -> Bool
    next x = if x < maxBound then not x else undefined

luochen1990

The Concept of Totality

See the definition of partial function in wikipedia

Total Function & Partial Function

examples of total functions:

luochen1990

import GHC.Stack

-- | a wrapper function to make "last" from base traceable
last' :: HasCallStack => [a] -> a
last' xs = case xs of [] -> error "abuse last"; _ -> last xs

-- | a untraceable partial function
foo :: [Int] -> Int
foo xs = last' xs + 1

luochen1990

Data.Foldable

• foldr1
• foldl1
• maximum
• minimum
• maximumBy
• minimumBy

Data.List

• head

luochen1990

GET WAN IP Address

> nslookup myip.opendns.com. resolver1.opendns.com

...
Name: myip.opendns.com
Address: 101.69.24.2