Complexify the type system to support rank-1 polymorphic types and terms.
With polymorphic types now expressible,
the proto token workaround should be removable,
since every token should now be able to directly have a Type/Term,
thus no longer needing to be applied to a few others before having it.
As a consequence of merging Type and Term,
the symantic machinery will have to be moved to TeSym,
and thus also carried by Type. WIP.
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
Cleaner to support the constraints
in the various data types' Proj_TyConC
instead of the constraints'.
For instance, this avoids to require the IO TyConst
when using MonoFunctor.
Julien Moutinho [Thu, 24 Nov 2016 04:47:58 +0000 (05:47 +0100)]
Revamp the type system.
This is definitively much more correct, simple and powerful this way:
kinds are now properly handled,
type constraints capture is now quite neat,
and usable type variables should be possible.
Though the current code may seem obvious and natural
for the task at hand, it required
first to know that this was indeed this task that has to be done…
Indeed I was previously much more focused on the symantics part,
but this happened when I decided to put a day or two
to check if type inferencing would indeed be possible with the previous type system,
I rapidly convinced myself that I couldn't handle type variables as required,
so I then put aside the previous type system to work anew
from the main (mono)type of Top,
which also appears in Write You a Haskell:
data Type
= TVar TVar
| TCon String
| TArr Type Type
As in the previous type system,
I first tried to have Type indexing an Haskell type (h)
by using the usual GADTs way,
which was surprisingly possible for every kind:
once I realized this could be done through Proxy
(this definitively is a very important type
to compute with GHC's type system),
and found that the type application could be handled
with a type family, which could effectively let me build types
from an AST, the type family's result just stays abstract,
and GADTs put constraints in scope with it in them.
The Index GADT of GLambda was my inspiration to handle type constants
through a type list of them, and thus drop the previous approach
which was indexing types (and not type constants)
and required much more code.
I then tried to have Type always well-formed through GADTs,
my first attempt was (stupidly) to only check the arity,
then I realized it was not enough and introduced a Kind type.
At this point I was able to kindcheck an AST of a type,
but failed to replicate the previous approach to capture a Constraint,
hopefully I then tried (without much hope it would work)
to do the "obvious thing" (since this is what GHC does),
that is to add a type constraint kind into Kind,
which proved itself quite rewarding.
Surprisingly I've quickly found that introducing UnProxy
enables to capture Constraints which need to work on abstract types,
like (Eq a) to prove (Eq (Maybe a)).
Work ahead is to try to update the previous approach
to build expressions with symantics.
Then later to try again type inferencing.
sourcephile / git / haskell / symantic.git / log