zmactep

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

Church Encoding

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -> (f (f x)))

xgrommx

{-# LANGUAGE StandaloneDeriving, DataKinds, PolyKinds, GADTs, RankNTypes, TypeOperators, FlexibleContexts, TypeFamilies, KindSignatures #-}

-- http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html

module HRecursionSchemes where

import Control.Applicative
import Data.Functor.Identity
import Data.Functor.Const
import Text.PrettyPrint.Leijen hiding ((<>))

johnchandlerburnham

A Taxonomy of Self-Types

Part I: Introduction to Self-Types

Datatypes in the Formality programming language are built out of an unusual structure: the self-type. Roughly speaking, a self-type is a type that can depend or be a proposition on it's own value. For instance, the consider the 2 constructor datatype Bool:

sheaf

{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MagicHash                #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE NamedWildCards           #-}
{-# LANGUAGE PatternSynonyms          #-}
{-# LANGUAGE PartialTypeSignatures    #-}