laughinghan

• any: magic, ill-behaved type that acts like a combination of never (the proper [bottom type]) and unknown (the proper [top type])
  • Anything except never is assignable to any, and any is assignable to anything at all.
  • Identities: any & AnyTypeExpression = any, any | AnyTypeExpression = any
  • Key TypeScript feature that allows for [gradual typing].
• unknown: proper, well-behaved [top type]
  • Anything at all is assignable to unknown. unknown is only assignable to itself (unknown) and any.
  • Identities: unknown & AnyTypeExpression = AnyTypeExpression, unknown | AnyTypeExpression = unknown

• Prefer over any whenever possible. Anywhere in well-typed code you're tempted to use any, you probably want unknown.

bishboria

These links no longer work. Springer have pulled the free plug.

Graduate texts in mathematics

duplicates = multiple editions

A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen

A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen

mrb

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Nat) -> GCounter

gcjoin : GCounter -> GCounter -> GCounter
gcjoin l r = (MkGCounter (maximum (value l) (value r)))

mxswd

// this is a playground
protocol Nat {
  class func construct() -> Self
  class func value() -> Int
}

struct Z : Nat {
  static func construct() -> Z {
    return Z()
  }

mrb

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Nat) -> GCounter

natMax : Nat -> Nat -> Nat
natMax Z m = m
natMax (S n) Z = S n

andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

puffnfresh

module LoobVerifiedMonoid

data Loob = Eurt | Eslaf

instance Semigroup Loob where
  Eurt <+> _ = Eurt
  Eslaf <+> r = r

instance Monoid Loob where
  neutral = Eslaf

david-christiansen

module ErrorTest

import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

data Ty = TUnit | TFun Ty Ty

mvr

A Whirlwind Tour of Combinatorial Games in Haskell
==================================================

Combinatorial games are an interesting class of games where two
players take turns to make a move, changing the game from one position
to another. In these games, both players have perfect information
about the state of the game and there is no element of chance. In
'normal play', the winner is declared when the other player is unable
to move. A lot of famous strategy games can be analysed as
combinatorial games: chess, go, tic-tac-toe.

voila

module Date

-- leap year ?
leap : Integer -> Bool
leap year = (mod year 4 == 0) && ((mod year 400 == 0) || not (mod year 100 == 0))

-- number of days in month/year
days : Integer -> Integer -> Integer
days 2     year = if leap year then 29 else 28 
days month _    = if month `List.elem` [4,6,9,11] then 30 else 31