Opened 4 years ago

Last modified 4 years ago

#1675 new proposed-project

A substitution stepper

Reported by: Freinn Owned by: Freinn
Priority: not yet rated Keywords: substitution stepper expressions lambda calculus
Cc: Difficulty: unknown
Mentor: not-accepted Topic: Tools

Description

This idea was in my head since people learning haskell (like me) usually have some trouble understanding substitution step by step. Is the third wish in ​http://chrisdone.com/posts/haskell-wishlist

Example:

foldr (+) 0 [1, 2, 3, 4]

foldr (+) 0 (1 : [2, 3, 4])

1 + foldr (+) 0 [2, 3, 4]

1 + foldr (+) 0 (2 : [3, 4])

1 + (2 + foldr (+) 0 [3, 4])

1 + (2 + foldr (+) 0 (3 : [4]))

1 + (2 + (3 + foldr (+) 0 [4]))

1 + (2 + (3 + foldr (+) 0 (4 : [])))

1 + (2 + (3 + (4 + foldr (+) 0 [])))

1 + (2 + (3 + (4 + 0)))

1 + (2 + (3 + 4))

1 + (2 + 7)

1 + 9

10

Comparing this with foldl immediately shows the viewer how they differ in structure:

foldl (+) 0 [1, 2, 3, 4]

foldl (+) 0 (1 : [2, 3, 4])

foldl (+) ((+) 0 1) [2, 3, 4]

foldl (+) ((+) 0 1) (2 : [3, 4])

foldl (+) ((+) ((+) 0 1) 2) [3, 4]

foldl (+) ((+) ((+) 0 1) 2) (3 : [4])

foldl (+) ((+) ((+) ((+) 0 1) 2) 3) [4]

foldl (+) ((+) ((+) ((+) 0 1) 2) 3) (4 : [])

foldl (+) ((+) ((+) ((+) ((+) 0 1) 2) 3) 4) []

(+) ((+) ((+) ((+) 0 1) 2) 3) 4

1 + 2 + 3 + 4

3 + 3 + 4

6 + 4

10

Each step in this is a valid Haskell program, and it’s just simple substitution.

This would be fantastic for writing new algorithms, for understanding existing functions and algorithms, writing proofs, and learning Haskell.

Change History (1)

comment:1 Changed 4 years ago by Freinn

Type: spam β†’ proposed-project
Note: See TracTickets for help on using tickets.