inkytonik / cooma

The Cooma project is investigating secure programming language design based on fine-grained object capabilities.
Mozilla Public License 2.0
3 stars 2 forks source link

features/types #49

Closed inkytonik closed 3 years ago

inkytonik commented 3 years ago

A few type analysis fixes

nhweston commented 3 years ago

Both of these are probably beyond the scope of what we want to be doing right now, so happy to merge if you are.

Higher-kinded types

Higher-kinded types still cause crashes:

cooma> type Apply = fun (F : (Type) Type, A : Type) F(A)
Apply : (F : (Type) Type, A : Type) Type = <function>

cooma> Apply(Option, Int)
Exception in thread "main" org.bitbucket.inkytonik.kiama.relation.NodeNotInTreeException: node not in tree: Idn(IdnUse(F))
    at org.bitbucket.inkytonik.kiama.relation.TreeRelation.apply(TreeRelation.scala:53)
…
cooma> fun (F : (Type) Type, x : F(Int)) x
Exception in thread "main" java.lang.RuntimeException: checkInput: couldn't find REPL type for REPLExp(Fun(Arguments(Vector(Argument(IdnDef(F),FunT(ArgumentTypes(Vector(ArgumentType(None,Idn(IdnUse(Type))))),Idn(IdnUse(Type))),None), Argument(IdnDef(x),App(Idn(IdnUse(F)),Vector(Idn(IdnUse(Int)))),None))),Idn(IdnUse(x))))
    at scala.sys.package$.error(package.scala:27)
    at org.bitbucket.inkytonik.cooma.REPL.checkInput(REPL.scala:152)
…

Vector type constructor

The special treatment of Vector still causes some behaviour inconsistent with other type constructors:

cooma> Option
Option : (T : Type) Type = <function>

cooma> Vector
'(' expected
Vector
      ^
inkytonik commented 3 years ago

Thx. Yeah, I think we can live with those issues for now.