joshcough

{-# LANGUAGE GADTs, ConstraintKinds, Rank2Types, ImplicitParams #-}

data Rec fields where
  Rec :: fields => Rec fields

infixr 1 ?
(?) :: Rec fields -> (fields => r) -> r
Rec ? e = e

record :: Rec (?a :: Int, ?b :: String)

joshcough

Direct links to free Springer maths books (pdf versions)

duplicates = multiple editions

A Classical Introduction to Modern Number Theory,Kenneth IrelandMichael Rosen

A Classical Introduction to Modern Number Theory,Kenneth IrelandMichael Rosen

A Course in Arithmetic,Jean-Pierre Serre

joshcough

module Foo where

import Debug.Trace

traceByteString :: String -> ByteString -> ByteString
traceByteString msg b | traceShow b False = undefined
traceByteString msg b = b

joshcough

This is material to go along with a 2014 Boston Haskell talk.

We are going to look at a series of type signatures in Haskell and explore how parametricity (or lack thereof) lets us constrain what a function is allowed to do.

Let's start with a decidedly non-generic function signature. What are the possible implementations of this function which typecheck?

wrangle :: Int -> Int

joshcough

module Infer where

import Control.Monad.State
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

data Var = V {-# UNPACK #-} !Int (Maybe String)

data HM = HM
    { nextVar :: {-# UNPACK #-} !Int

joshcough

{
{-# OPTIONS -w  #-}
module CoreLexer
( Alex(..)
, AlexPosn(..)
, Token(..)
, alexMonadScan
, runAlex
, alexGetInput
) where