• Stars
    star
    131
  • Rank 275,867 (Top 6 %)
  • Language Idris
  • License
    Other
  • Created over 3 years ago
  • Updated about 3 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Idris version of Domain Modeling Made Functional Book.

Idris Full Stack DDD NodeJS example

Order Taking Service

Idris version of Domain Modeling Made Functional Book.

The Domain Modeling Made Functional by Scott Wlaschin introduces domain driven design and shows how well it fits to the world of functional programming via the lens of the F# programming language. As Scott showed us that DDD is indeed a nice fit for functional programming, questions arise naturally; could we push further the abstractions if we use a dependently typed programming language, like Idris? Where are the sweet spots of depedent types in the world of everyday programming? Everyday programming needs to be focused on delivery, maintanability, reliability, and being correct. The sad truth is that many applications needs to be more maintanable than correct. Being correct is not a clear concept because its meaning changes as the software evolves. In many cases, stakeholders only get a deeper understanding of the domain as the software solution/product evolves over time. In this setting, depedent typed programming helps us achieve maintanability rather than being correct. In this repository I show a simple layered architecture and I show how to use simple dependent types to draw explicit connections between the high level design of a service and its NodeJS deployed implementation. Ideas and practices originated, but reshuffled from the Type Driven Development with Idris by Edwin Brady and the Domain Modeling Made Functional by Scott Wlaschin. This architecture includes; An abstraction to talk about Bounded Context and Workflow, type safe description of a state transition system, a free monad approach for domain implementation, and an actual implementation of the domain on NodeJS back-end. Because of dependent types, this architecture becomes explicit, rather than implicit, meaning that connections between the high level design and the low level implementation are done via functions, changing the code anywhere requires to think at the whole, as possible type errors propagates to top or to bottom. Idris could immensely benefit from simple FFIs for NodeJS libraries. The FFIs would grant access to thousands of libraries from the NodeJS ecosystem almost for free. This approach would position Idris to be used even in production settings and the Idris userbase could be bootstrapped, later the Idris version of these libraries could be written.

Request: Please consider buying both of the books mentioned above. Boths are excellent resources for further studying of the applied subject.

Work In Progress parts:

  • The documentation is still under development. Please come back regurarly to see what changed.
  • Client needs lots of improvements.
  • Better error Handling around workflow runners.
  • Dependently driven testing needs to be implemented.

Financial Support

Talk

Youtube

Notes

This project meant to be a blue-print, example for micro-services written in Idris. Its main focus is to reproduce abstractions in dependently typed setting, that can be found in Scott Wlashin's book. The main focus is around the dependently typed implementation of BoundedContext, but several other parts of the architecture had to be worked on to be able to demostrate that Idris can host such solutions. Although during the implementation many other problems were required to think about in the dependently typed setting. This repository can be considered as a mine practices for dependently typed software development. Enjoy digging up those gems.

You may find the style of the explanations strange, maybe a bit chaotic, but if you follow path suggested in the READMAP.md you will learn many things about the Idris language. This style feels chaotic that could be because I have a slight ADHD and I try to linarize the content here, but sometimes quickly the explanations go deep. Although I believe a short explanation after every Idris snippet helps to view this reposity as a hand-book for Idris development.

High level overview

This repository contains more than just the Idris one to one translation of the F# code from the Domain Modeling Made Functional book. I wanted to show how Idris can be used to interface with existing NodeJS libraries. For that reason I added the following parts:

  • FFI for NodeJS interfacing libraries
  • Sketch of type-safe SQL library
  • Minimal scaffolding of a NodeJS server
  • Dependently typed framework for Bound-Context and Workflows
  • State transition of the PlaceOrder example
  • Free monadic DSL formalization of the PlaceOrder example
  • One backend implementation of the operations of PlaceOrder DSL

See the slides

Run

After setted up; start the microservice with make start-opt, start the client service npm run dev, and open localhost:5000 in a browser.

Setup

Server

  • Install Idris2 which version must match the one marketd the VERSIONS file. OR
  • If you Idris2 release version installed, check out the corresponding tag from 0.4.0

For dependencies install nodejs, npm and packages:

npm install google-closure-compiler
npm install sqlite
npm install md5

To start the OrderTaking service, which will create the initial Sqlite DB and starts the service on 127.0.0.1:3000

make init-db
make start-opt

Client

An example client can be found in the client/svelte-client directory. Follow the instructions from its README.md

To run the client, call the following command:

cd client/svelte-client
npm run dev

Which starts the client in development mode, any changes in its code, will be picked up.

Important note, use the g21 as product code on the client side for testing. The client is very in pre-alpha state, best to open the developer console to see, what happens before and after submitting the order. I will work on these details soon.

Have fun!

ASCII ART

ASCII ART

More Repositories

1

mini-grin

ICFP tutorial
Haskell
40
star
2

IdrisExtSTGCodegen

Idris
24
star
3

TaPL

TaPL implementation bits in Idris2
Idris
15
star
4

pearls

Some functional pearls from time to time
Haskell
8
star
5

bead

E-learning snap based server for special teaching purposes
Haskell
7
star
6

py-contract

Simple examples from category theory using Python
Python
6
star
7

ArchaIdr

Classic Arcade games written in Idris compiled to JavaScript.
HTML
3
star
8

cpdt

Certified Programming with Dependent Types - examples, learning material.
Coq
2
star
9

oo-haskell

How Object Oriented programming can be encoded in Haskell
Haskell
2
star
10

advent-of-code

Idris
2
star
11

lentil

Access database entities through lenses.
Haskell
2
star
12

PLFI

Programming Language Foundations in Idris
Idris
2
star
13

LearningCoq

Coq exercises.
Coq
2
star
14

DepPy

Imagine a Dependently Typed Python
Python
2
star
15

themis

Simple Testing Framework, for Interactive and Unit testing
Haskell
1
star
16

PFDSI

Idris
1
star
17

air

Air (Albérlet Irányítási Rendszer) aka Flat Accounting System
Haskell
1
star
18

dmmf

Examples from the 'Domain Modeling made Functional' book.
Idris
1
star
19

hackerrank

Haskell
1
star
20

file-persist

File storage backend for the Haskell persistent package.
Haskell
1
star
21

subtitles

Simple Ass to Srt subtitle converter
Haskell
1
star
22

HtDP2

How to Design Programs 2 from EDX combined with shape functors and anamorphisms
Haskell
1
star
23

spd

Simple Framework for creating reactive programming examples based on the How to Design Programs book
Haskell
1
star
24

aoc2022

Advent of Code 2022
Idris
1
star
25

elim

Generic eliminators for ADTs
Haskell
1
star
26

category-test-laws

Algebraic laws and QuickCheck properties of Haskell constructions.
Haskell
1
star
27

CrackingTheCodingInterview

Haskell
1
star
28

hs-bluesnap

hs-bluesnap
Haskell
1
star
29

idris-ct-studies

Basic category theory studies in Idris2
Idris
1
star
30

TheRayTracerChallenge

Idris
1
star