hexresearch / hschain-utxo

UTXO-based contracts for hschain
0 stars 0 forks source link

Refactor type check #211

Closed anton-k closed 3 years ago

anton-k commented 3 years ago

Refactors type-checker package. Constraints for type-inference functions look too monstrous and I've made common type class Lang that simplifies contexts and types.

class
   ( IsVar (Var q)
   , Show (Src q)
   , Eq (Src q)
   ) => Lang q where

   -- | Variables for our language. Notice that this type should be injective in relation to type of @Lang@.
   -- We need to have unique type of variables for each language definition.
   type Var q = r | r -> q

   -- | Source code locations
   type Src q

   -- | Primitives
   type Prim q

   -- | Reports type for primitive.
   getPrimType :: Prim q -> TypeOf q

-- | Types of our language
 type TypeOf q = Type (Src q) (Var q)

 -- | |Terms of our language
 type TermOf q = Term (Prim q) (Src q) (Var q)

 -- | Typed terms of our language
 type TyTermOf q = TyTerm (Prim q) (Src q) (Var q)

 -- | Type errors of our language
 type ErrorOf q = TypeError (Src q) (Var q)

 -- | Type substitutions
 type SubstOf q = Subst (Src q) (Var q)

With the help of this class and type synonyms signature for type-inference function becomes more user-friendly:

inferTerm :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TyTermOf q)

Also this PR eliminates a hack for allocation of fresh-variables. We made them with convertion from int and added some hackery prefix "$$". In this PR this is no longer needed. Internaly we use wrapper:

data Name var
  = Name var
  | Fresh Int

And with last stage we eliminate all int's by substitution with cannonical pretty variables which user provides in the instance of class IsVar.

Also renamed package with better name and to not to interfere with module names of original package hindley-milner.

Adds docs and examples.