RSolve: A general solver for equations

[ library, logic, mit, program, unification ] [ Propose Tags ]

A general solver for type checkers of programming languages and real world puzzles with complex constraints.

[Skip to Readme]
Versions [faq],,
Dependencies base (==4.*), containers [details]
License MIT
Copyright 2018 thautwarm
Author thautwarm
Category Language
Home page
Source repo head: git clone
Uploaded by ice1000 at 2018-12-25T07:46:00Z
Distributions NixOS:
Downloads 1141 total (5 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2018-12-25 [all 1 reports]


[Index] [Quick Jump]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for RSolve-

[back to package description]


A general solver for type checkers of programming languages and real world puzzles with complex constraints.


Here are 2 special cases presented in the following sections to show how powerful RSolve is.

The Most Graceful Hindley-Milner Unification

Check RSolve.HM.Core and RSolve.HM.Example.

Uncomment the code in Main.hs could reproduce following program:

check = do
    let i = Prim Int
    let f = Prim Float
    let arrow = Op Arrow i f
    -- u means undecided
    u1 <- new
    u2 <- new
    u3 <- new
    u4 <- new
    -- u1 -> u2 where u1, u2 is not generic
    let arrow_var = Op Arrow (Var u1) (Var u2)
    -- int -> int
    let arrow_inst1 = Op Arrow i i
    -- float -> float
    let arrow_inst2 = Op Arrow f f
    -- a generic function
    let arrow_generic = Forall [u3] $ Op Arrow (Var u3) (Var u3)

    let arrow_match = Op Arrow (Var u4) (Var u4)

    _ <- solve $ Unify arrow arrow_var
    _ <- solve $ Unify arrow_inst1 arrow_match
    _ <- solve $ Unify arrow_generic arrow_inst1
    _ <- solve $ Unify arrow_generic arrow_inst2
    _ <- solveNeg

    mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]


u1 : Int
u2 : Float
arrow_inst1 : (Int -> Int)
arrow_inst2 : (Float -> Float)
arrow_generic : forall  a2.(a2 -> a2)
arrow_match : (Int -> Int)

N-Option Puzzles

This implementation is presented at RSolve.Options, which provides the abstractions to solve all kinds of puzzles described with options.

A Hello World program could be found at src/Main.hs which solves a complex problem described with following link:

However, the much easier cases taking the same background as above problem (logic constraints described with four options A, B, C, D) could be enjoyale:

test2 = do
  a <- store $ sol [A, B, C]
  b <- store $ sol [B, C, D]
  c <- store $ sol [C]
  _ <- solve $ a `eq`  b
  _ <- solve $ b `neq` c
  _ <- solveNeg  -- `Not` condition requires this
  _ <- solvePred -- unnecessary
  mapM require [a, b, c]

main = do
    format ["a", "b", "c"] . nub . fst
    $ runBr test2 emptyLState


λ stack exec RSolve
"a" : Sol (fromList [B])
"b" : Sol (fromList [B])
"c" : Sol (fromList [C])