dope2/progress.txt
2025-03-23 09:15:37 +01:00

72 lines
2.4 KiB
Text

status:
- 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.
todo:
- rename Type to a NominalType?
const nominalType = (name, params) => ({left: name, right: params});
type of every nominal type is (String, [Type])
- 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?