branching and very basic merging of slots

This commit is contained in:
Joeri Exelmans 2025-04-17 09:19:41 +02:00
parent 614e6c0fdb
commit 3978f7f835
32 changed files with 684 additions and 420 deletions

View file

@ -1,72 +1,24 @@
status:
done:
- everything is properly typed, up to the meta-circular level
- primitives
- structures: list, product, sum
can compose structures, e.g., create list of list of product of sum of ...
list type is specialized for ListOfByte to use Uint8Array
- generics currently implemented in two ways:
1) similar to "templates" (as in C++):
a generic function or type is a function that takes a Type, and produces a specific variant
2) experimental implementation of polymorphic types and type inferencing
values currently treated as white-box, hardcoded generic types (e.g., list, function) in type inferencing algorithm
wip:
- interfaces via typeclasses?
- revise the way types are encoded
we need only one 'type of type' (called 'kind' in Haskell), and we can call it 'Type'.
types explicitly contain their underlying types. the type inferencing algorithm needs this information.
Int
{ symbol: Int, params: [] }
[Int]
{ symbol: List, params: [{ symbol: Int, params: [] }] }
[[Int]]
{ symbol: List,
params: [{ symbol: List, params: [{symbol: Int, params: []}]}]}
Int -> Bool
{ symbol: Function, params: [
{ symbol: Int, params: [] },
{ symbol: Bool, params: [] },
]
}
Int | Bool
{ symbol: Sum, params: [
{ symbol: Int, params: [] },
{ symbol: Bool, params: [] },
]
}
(Int, Bool)
{ symbol: Product, params: [
{ symbol: Int, params: [] },
{ symbol: Bool, params: [] },
]
}
Point2D <-- custom nominal type! maybe it contains two Doubles, but we don't expose this
{ symbol: Point2D, params: [] }
Type constructors are just functions that return a 'Type'.
For instance:
lsType :: Type -> Type
fnType :: Type -> Type -> Type
The sad(?) part about all of this, is that I'm converging with Haskell/Lean.
can compose structures, e.g., create list of list of product of sum of ...
list type is specialized for ListOfByte to use Uint8Array
- generic types and type inferencing
todo:
- rename Type to a NominalType?
const nominalType = (name, params) => ({left: name, right: params});
type of every nominal type is (String, [Type])
- to support sets of slots, need comparison of slots
=> comparison of values
=> problem: how to compare transformed values? their inputs can come from different types
(a) tedious: put in every value:
- the type
- a comparison function for that type
then first compare types, if types match, compare values.
could generalize this by writing a compare function on 'typed' values.
(b) dirty: use 'magic' function that compares any JS value
- typeclass mechanism
- what about type links: they connect anything to its type... what is the type of 'anything'?
- treat all values as polymorphic? (non-polymorphic values simply have empty set of type variables)
- type inferencing can be reduced to finding a graph isomorphism?