paf31

module Main where

import Debug.Trace

import Data.Tuple
import Data.Either
import Data.Lazy

class Memo a where
  memo :: forall r. (a -> r) -> a -> Lazy r

paf31

module Main where

import qualified Prelude as P
import Debug.Trace

class Arithmetic lang where
  (+) :: lang Number -> lang Number -> lang Number
  (-) :: lang Number -> lang Number -> lang Number
  (*) :: lang Number -> lang Number -> lang Number
  (/) :: lang Number -> lang Number -> lang Number

paf31

{-# LANGUAGE FunctionalDependencies, DataKinds, GADTs, PolyKinds, KindSignatures, MultiParamTypeClasses #-}

module Main where

import Data.Monoid

import Prelude (Maybe(..))
import qualified Prelude as P

class Category (arr :: k -> k -> *) where

paf31

module Main where

-- We will define our checker by piecing together functions based on the various types of binders.
-- We use prisms to abstract over the data constructors representing binders
type Prism a b = (a -> b, b -> Maybe a)

-- As an example, suppose we want to check array binders [_, _, ..., _] for exhaustivity.
-- We could introduce two constructors ArrNil and ArrCons, and require these constructors be
-- binders in our language.
data Array b = ArrNil | ArrCons b b deriving (Show)

paf31

module Tree where

data Binder = Wildcard | Zero | Succ Binder deriving (Show)

data Tree = Covered | Uncovered | Branch Tree Tree

color :: Tree -> Binder -> Tree
color _            Wildcard = Covered
color Covered      _        = Covered
color Uncovered    Zero     = Branch Covered Uncovered

paf31

# empty and unit types

type (Void,,,) = lfix id
type (Unit,MakeUnit,) = Void -> Void
data Unique = MakeUnit id

# natural number type

type (Nat,MakeNat,UnmakeNat,FoldNat) = lfix const Unit + id

paf31

# Iterate a function n times
data Iterate = f => FoldNat <const id, g => $g . $f>

# Subtract a number by iterating the predecessor function
data Sub = Iterate Pred

# Test whether a natural number is zero or non-zero
data IsZero = <const True, const False> . UnNat

# Test whether or not two natural numbers are equal

paf31

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PolyKinds #-}

> import Data.List

The following type definition will be lifted to the kind level, generating two constructors Z :: Nat and S :: Nat -> Nat

> data Nat = Z | S Nat

> _1 = S Z

paf31

In this post, I'd like to revisit Algorithm W, which I discussed when I wrote about Purity's typechecker.

Recalling the approach taken before, a term was typed by collecting constraints between unknown type variables by traversing the term in question, and then solving those constraints by substitution. This time I'd like to generalize the second part of the algorithm, to solve constraints over any term functor by substitution.

> {-# LANGUAGE EmptyDataDecls #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE FlexibleInstances #-}

> module Solver where

paf31

In the following, I will write a polykinded version of the combinators fold and unfold, along with three examples: folds for regular datatypes 
(specialized to kind *), folds for nested datatypes (specialized to kind * -> *), and folds for mutually recursive data types (specialized to 
the product kind (*,*)). The approach should generalise easily enough to things such as types indexed by another kind (e.g. by specializing to 
kind Nat -> *, using the XDataKinds extension), or higher order nested datatypes (e.g. by specializing to kind (* -> *) -> (* -> *)).

The following will compile in the new GHC 7.4.1 release. We require the following GHC extensions:

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE KindSignatures #-}