时间戳

首页 > 解决方案 > 如何在 Haskell 中使用 GADT 更改类型

haskell - 如何在 Haskell 中使用 GADT 更改类型

问题描述

按照https://stackoverflow.com/a/26084087/8142021中的答案， 我使用以下 haskell 代码来定义带有 GADT 的模态逻辑。

data Plain
data Mod
data Formula t where
   Prop :: {propName :: String} -> Formula t
   Neg  :: Formula t -> Formula t
   Conj :: Formula t -> Formula t -> Formula t
   Disj :: Formula t -> Formula t -> Formula t
   Impl :: Formula t -> Formula t -> Formula t
   BiImpl :: Formula t -> Formula t -> Formula t
   MyModality :: Formula Mod -> Formula Mod 

type PlainFormula = Formula Plain
type ModalFormula = Formula Mod

有没有办法将 PlainFormula 的类型更改为 ModalFormula？由于 PlainFormula 是 Modal Formula 的一个子集，我尝试定义以下注入但它不起作用。

toModal :: PlainFormula -> ModalFormula
toModal f = f

标签： haskellgadt

解决方案

推荐阅读