![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
Open issues list:
---
proposals:
---
'vague types': e.g. 'real number' or 'date' or 'time delta'. These are things that in theory have a precise definition but cannot be or cannot be efficiently represented, and in addition may (or may not, in the case of 'real number') have different units.
in order to make it into a normal CS type, you may need to add a unit, and you need to add a representation (how it is represented in bits in memory, and how the encapsulated operations can be performed on those), and in addition, you may need to change the semantics to deal with implementation issues, e.g. for real numbers you need to limit precision somehow (not always in a fixed way, e.g. IEEE 754 floating point), and you also need to limit range somehow (e.g. CS floating points and ints have a max and a min), and maybe you need to specify behavior for dealing with these things (e.g. if you are at the max and you add 1, does it wrap around? if you add a too-tiny value, does nothing happen?) And maybe you need to specify things like NaNs?, too.
note that with this conception, even various abstract perfect types can be reconceptualized as implementations of other abstract perfect types, e.g. ints are like an imprecise implementaion of floats, and finite fields are like a way of handing overflow in ints. This means there are embeddings between them, e.g. 0 == 0.0
---
perhaps there is a place for hoon's odors vs. structural types in oot
---
current proposal to prevent black magic like the Haskell variadic function example (http://stackoverflow.com/questions/3467279/how-to-create-a-polyvariadic-haskell-function ; see ootTypeNotes2):
just ban output ad-hoc polymorphism altogether and use type parameters for things like 'default'?
---
how to make types simple? note that:
(a) they are structural patterns/gregexs, (b) they are graphs themselves (eg. a -> (b -> c) clearly has a graph shape)
---
so i guess Oot should allow the user to define 'custom atomic types'
some fundamental atomic types:
composite types (subsumed into graphs):
---
---
consider 'fmap'; a function that takes two arguments, a container and a function, and applies the function to everything in the (flattened) container. The container must support an interface, call it 'fmappable' or 'flattenable' (depending on how it works) that knows how to flatten it.
But what if there are two implementations of this interface for a given data type? Eg for a binary tree you could say, fmap applied to a node could either apply the function to each of its descendent nodes, or only to its descendent leaf nodes (a third alternative could be to apply it only to the immediate children, not all descendents, eg fmap would be the same as map in this one). This is the 'coherence'-related problem in Haskell. In Oot we want to be able to implement the same interface in different ways on the same datatype, eg 'add' on an integer could be standard integer arithmetic or modular arithmetic; integers could be compared in the usual way, or by the subset relation on their prime factors; etc.
One could resolve this via Views. Eg one View of a binary tree type would use the fmap interface that applies to only the leaf nodes, while another View of the same binary tree type would use the fmal interface that applies to all interior nodes.
One could even define a View as an assignment of various concrete implementations to various interfaces (although i guess it is also a type; but what is a type but a set of interfaces that must be supported? well, i guess a type is also (a) a set of values, and (b) an algebraic thingee, eg the 'list' type constructor applies to the 'Int' type to produce list of Ints).
also a type could be (c) 'structural types', which is sort of the same as a list of interfaces, and (d) the set of things that have some attribute or tag (possibly a meta-attribute) such as 'things with units of meters' or 'tall people' or 'rabbits (objects which are animals of species rabbit)'.
---
https://andreacensi.github.io/contracts/ looks great. Summary:
three syntaxes:
@contract(a='int,>0', b='list[N],N>0', returns='list[N]') def my_function(a, b): ...
@contract def my_function(a : 'int,>0', b : 'list[N],N>0') -> 'list[N]': # Requires b to be a nonempty list, and the return # value to have the same length.
@contract def my_function(a, b): """ Function description. :type a: int,>0 :type b: list[N],N>0 :rtype: list[N] """ ...
Extensions: You can extend PyContracts? with new contracts types:
new_contract('valid_name', lambda s: isinstance(s, str) and len(s)>0) @contract(names='dict(int: (valid_name, int))') def process_accounting(records): ...
Any Python type is a contract:
@contract(a=int, # simple contract b='int,>0' # more complicated ) def f(a, b): ...
@contract(image='array[HxWx?3](uint8),H>10,W>10') def recolor(image): ...
related: here's a package to have validation schemas for dicts: http://valedictory.readthedocs.io/en/latest/
---
i guess that since we want everything to be a graph (and we want, Clojure-style fewer data types with common operations on them, rather than, Haskell style, many incompatible data types, one for each usage), we'll be passing around tables a lot where eg Haskell would pass an ADT or Python would pass a class instance. Which means that one will often be doing things that desugar to table.get("fieldname"). But we do want the static type system to ensure whether or not "fieldname" exists on this table, for both safety reasons (no runtime KeyError? in what would, in another language, be an access of a field in a class instance), and performance (the compiler can implement this table as a struct rather than a hash table).
So we have the ability for the type system to guarantee that some particular table lookup will always succeed. Given this, for convenience, the programmer doing this lookup shouldn't have to check to failure. That is, where table lookups might result in the None of an Option type, but the lookup is guaranteed to succeed, the compiler should allow the Option type to be replaced by the type it wraps (the value type of the table), and where table lookups might result in KeyErrors? being thrown, the type system should represent that in cases where the table is statically guaranteed to have the key, no keyerror might be thrown by the lookup.
---
i think we want row polymorphism instead of structural subtyping:
" Here's a simple example of where the row instantiation can cause differences:
let f x = x with {sum: x.a + x.b} let answer = f {a: 1, b: 2, c: 100}
With structural subtyping, the type is upcast to what f needs and we get back:
answer :: {a: Number, b: Number, sum: Number}
But with row polymorphism, ...
answer :: {a: Number, b: Number, c: Number, sum: Number} " -- https://brianmckenna.org/blog/row_polymorphism_isnt_subtyping
---
mb call it 'bit' instead of bool b/c shorter. Although for err stuff we'll be using a 'trit' instead, but let's call that a 'tri' b/c same number of letters as bit.
---
