plusOne : Nat -> Nat
map : (a -> b) -> (functor:Functor) a -> functor b
When the type of map plusOne gets calculated, the type of plusOne gets "plugged" into (a -> b). We can deduce from this that a should be bound to Nat and that b should be bound to Nat.
The expected result from bnd "Nat -> Nat" "a -> b" should thus be { a --> Nat, b --> Nat}.
We can then further substitute this binding in the rest of the type expression:
If you get a faulty result, please report here.
If you modify the source code (workspace/Data/src), please commit and push if it is usefull code; if these are toys and only for testing, make a new branch.
TODO
[x] Fix bug that too much is returned (e.g. Eq, even that List a is not Eq - List (a:Eq) is Eq btw)
[ ] Report cyclic binds/infinite types, e.g. {a --> List a}
[x] Optimize for speed! It is a disaster now. E.g. caching types into the state monad
[x] Normalize RSTT, so that "List" --> "Collection"
Please test supertype and bind.
How?
Now, type
supers "List a"to see all the supertypes ofList a", being{Collection a, Monoid, Mappable}(and more)Type
bind "List Nat" "List a"to see the binding calculated or a error message if binding failed.Consult the list of types, especially the supertypetable
What is binding?
When the type of
map plusOnegets calculated, the type ofplusOnegets "plugged" into(a -> b). We can deduce from this thatashould be bound toNatand thatbshould be bound toNat.The expected result from
bnd "Nat -> Nat" "a -> b"should thus be{ a --> Nat, b --> Nat}.We can then further substitute this binding in the rest of the type expression:
How to report?
Experiment at will!
If you get a faulty result, please report here. If you modify the source code (
workspace/Data/src), please commit and push if it is usefull code; if these are toys and only for testing, make a new branch.TODO
Eq, even thatList ais notEq-List (a:Eq)isEqbtw){a --> List a}