hexresearch / hschain-utxo

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

Семантика и типобезопасность ECase & EConstr #54

Closed Shimuuar closed 3 years ago

Shimuuar commented 4 years ago
  | ECase !(Typed Expr) [CaseAlt]
  | EConstr Type !Int !Int

Легко видеть, что EConstr совершенно не типобезопасен. В него можно вписать любой тип. Точно также ECase не проверяет, что разбор паттерна корректен. Так пример с их помощью можно легко написать unsafeCoerce:

unsafeCoerce :: Type -> Type -> Scomb
unsafeCoerce tyA tyB = Scomb
  { scomb'name = "unsafeCoerce"
  , scomb'args = V.fromList [Typed "a" tyA]
  , scomb'body = Typed
    { typed'value = ECase
      (Typed 
       (EAp (EConstr (arrowT tyA tyA) 0 1) (EVar "a"))
       tyA
      )
      [CaseAlt 0 [Typed "b" tyB] (EVar "b")]
    , typed'type = tyB
    }
  }
λ> typeCheck preludeTypeContext [unsafeCoerce intT boolT]
True

И в целом нужно боле подробное описание того как constr/case работают.