Stack Overflow
Stack Overflow

Questions tagged [church-encoding]

Questions about the Church encoding, a way to represent data using functions, and the Boehm-Berarducci encoding, a transposition of it to a typed setting. For questions primarily about the related Scott and Mogensen-Scott encodings, there is [scott-encoding].

Related Tags: , .

93 questions
26
votes
3 answers

Church lists in Haskell

I had to implement the haskell map function to work with church lists which are defined as following: type Churchlist t u = (t->u->u)->u->u In lambda calculus, lists are encoded as following: [] := λc. λn. n [1,2,3] := λc. λn. c 1 (c 2 (c 3…
jcdmb
  • 3,016
  • 5
  • 38
  • 53
20
votes
3 answers

Subtraction of church numerals in haskell

I'm attempting to implement church numerals in Haskell, but I've hit a minor problem. Haskell complains of an infinite type with Occurs check: cannot construct the infinite type: t = (t -> t1) -> (t1 -> t2) -> t2 when I try and do subtraction. I'm…
Probie
  • 201
  • 2
  • 3
18
votes
3 answers

Arithmetic with Church Numerals

I am working through SICP, and the problem 2.6 has put me in something of a quandary. In dealing with Church numerals, the concept of encoding zero and 1 to be arbitrary functions that satisfy certain axioms seems to make sense. Additionally,…
afkbowflexin
  • 4,029
  • 2
  • 37
  • 61
18
votes
1 answer

What does "Error: Universe inconsistency" mean in Coq?

I am working through Software Foundations and am currently doing the exercises on Church numerals. Here is the type signature of a natural number: Definition nat := forall X : Type, (X -> X) -> X -> X. I have defined a function succ of type nat ->…
augurar
  • 12,081
  • 6
  • 50
  • 65
17
votes
2 answers

Lambda calculus in Haskell: Is there some way to make Church numerals type check?

I'm playing with some lambda calculus stuff in Haskell, specifically church numerals. I have the following defined: let zero = (\f z -> z) let one = (\f z -> f z) let two = (\f z -> f (f z)) let iszero = (\n -> n (\x -> (\x y -> y)) (\x y ->…
singpolyma
  • 10,999
  • 5
  • 47
  • 71
16
votes
2 answers

Why do we use folds to encode datatypes as functions?

Or to be specific, why do we use foldr to encode lists and iteration to encode numbers? Sorry for the longwinded introduction, but I don't really know how to name the things I want to ask about so I'll need to give some exposition first. This draws…
hugomg
  • 68,213
  • 24
  • 160
  • 246
14
votes
1 answer

Practical reasons for Church Encoding

Church encoding (aka Visitor Pattern) is a way of representing data as functions: instead of data T = C1 F1 F2 | C2 F3 F4 you can define data T = T (forall r. (F1 -> F2 -> r) -> (F3 -> F4 -> r) -> r) . Although the ability to represent anything as…
Rotsor
  • 13,655
  • 6
  • 43
  • 57
14
votes
3 answers

Is it possible to use church encodings without breaking equational reasoning?

Mind this program: {-# LANGUAGE RankNTypes #-} import Prelude hiding (sum) type List h = forall t . (h -> t -> t) -> t -> t sum_ :: (Num a) => List a -> a sum_ = \ list -> list (+) 0 toList :: [a] -> List a toList = \ list cons nil -> foldr cons…
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
13
votes
3 answers

More efficient tail of church encoded list

This is a literate haskell post. Simply save it as "ChurchList.lhs" to run it. > {-# LANGUAGE Rank2Types #-} A Church encoded list is a way of representing a list via a function. It resembles both folding and continuation passing style. > newtype…
PyRulez
  • 10,513
  • 10
  • 42
  • 87
12
votes
1 answer

Closures and universal quantification

I've been trying to work out how to implement Church-encoded data types in Scala. It seems that it requires rank-n types since you would need a first-class const function of type forAll a. a -> (forAll b. b -> b). However, I was able to encode pairs…
Apocalisp
  • 34,834
  • 8
  • 106
  • 155
10
votes
4 answers

How do I use the Church encoding for Free Monads?

I've been using the Free datatype in Control.Monad.Free from the free package. Now I'm trying to convert it to use F in Control.Monad.Free.Church but can't figure out how to map the functions. For example, a simple pattern matching function using…
Anupam Jain
  • 7,851
  • 2
  • 39
  • 74
10
votes
3 answers

Looking for a Church-encoding (lambda calculus) to define < , > , !=

I have to create some Lambda functions for > , < and != I don't have an idea how to , could anyone help me please ? PS: We just started with Lambda Calculus, so please do not assume any previous knowledge. Thank you in anticipation ! Edit - What I…
Blnpwr
  • 1,793
  • 4
  • 22
  • 43
10
votes
2 answers

Why are difference lists not an instance of foldable?

The dlist package contains the DList data type, which has lots of instances, but not Foldable or Traversable. In my mind, these are two of the most "list-like" type classes. Is there a performance reason that DList is not an instance of these…
Mike Izbicki
  • 6,286
  • 1
  • 23
  • 53
7
votes
2 answers

encoding binary numerals in lambda calculus

I have not seen any mention of binary numerals in lambda calculus. Church numerals are unary system. I had asked a question of how to do this in Haskell here: How to implement Binary numbers in Haskell But even after I saw and understood that…
Tem Pora
  • 2,043
  • 2
  • 24
  • 30
6
votes
2 answers

Sum/product of Church-encoded list of numbers does not type check

Following standard definitions of Church-encoded natural numbers and lists represented as right folds, I want to write a function that takes a list of numbers as its argument and returns sum of its elements: type Number = forall a. (a -> a) -> a ->…
shooqie
  • 950
  • 7
  • 17
1
2 3 4 5 6 7