解析索引类型

Question

我刚刚开始探索 data types à la carte in combination with indexed types. My current experiment is a bit too large to include here, but can be found here 的可能性。我的示例是将来自不同成分（算术、函数等）的表达式混合在一起。目标是只强制使用类型正确的表达式。这就是为什么将索引添加到表达式（Sort 类型）的原因。

我可以构建如下表达式：

-- define expressions over variables and arithmetic (+, *, numeric constants)
type Lia = IFix (VarF :+: ArithmeticF)

-- expression of integer type/sort
t :: Lia IntegralSort
t = var "c" .+. cnst 1

只要我只构造固定（静态）表达式，这一切都很好。

有没有办法从 string/other 表示中读取表达式（显然必须对排序进行编码）并生成由这些函子表示的动态值？

例如，我想阅读 ((c : Int) + (1 : Int)) 并用 VarF 和 ArithmeticF 以某种方式表示它。在这里我意识到我无法获取静态类型的值Lia IntegralSort。但是假设我还有：

data EqualityF a where
    Equals :: forall s. a s -> a s -> EqualityF a BoolSort

我希望有一个函数可以将 String 读入 Maybe (IFix (EqualityF :+: VarF :+: ...))。这样的函数将尝试为 LHS 和 RHS 构建表示，如果排序匹配，它可以产生静态已知类型 IFix (EqualityF :+: ...) BoolSort 的结果。问题是 LHS（和 RHS）的表示没有固定的静态排序。使用我选择的这种表示，我试图做的事情是不可能的吗？

Answer 1

(.=.) :: EqualityF :<: f => IFix f s -> IFix f s -> IFix f BoolSort
(.=.) a b = inject (Equals a b)

您可以使用 GADT 来隐藏排序，从而允许您 return 根据输入对值进行排序。然后模式匹配允许您恢复排序。

data Expr (f :: (Sort -> *) -> (Sort -> *)) where
  BoolExpr :: IFix f BoolSort -> Expr f
  IntExpr  :: IFix f IntegralSort -> Expr f

这是一个简单的后缀表达式解析器，涉及 + 和 =。

parse :: (EqualityF :<: f, ArithmeticF :<: f) => String -> [Expr f] -> Maybe (Expr f)

parse (c : s) stack | isDigit c =
  parse s (IntExpr (cnst (digitToInt c)) : stack)

parse ('+' : s) (IntExpr e1 : IntExpr e2 : stack) =
  parse s (IntExpr (e1 .+. e2) : stack)

parse ('=' : s) (IntExpr e1 : IntExpr e2 : stack) =
  parse s (BoolExpr (e1 .=. e2) : stack)

parse ('=' : s) (BoolExpr e1 : BoolExpr e2 : stack) =
  parse s (BoolExpr (e1 .=. e2) : stack)

parse [] [e] = Just e
parse _ _ = Nothing

您可能不喜欢 = 的重复案例。更通用的框架是 Typeable，允许您只测试所需的类型相等性。

data SomeExpr (f :: (Sort -> *) -> Sort -> *) where
  SomeExpr :: Typeable s => IFix f s -> SomeExpr f


parseSome :: forall f. (EqualityF :<: f, ArithmeticF :<: f) => String -> [SomeExpr f] -> Maybe (Expr f)

parseSome (c : s) stack | isDigit c =
  parseSome s (SomeExpr (cnst (digitToInt c)) : stack)

parseSome ('+' : s) (SomeExpr e1 : SomeExpr e2 : stack) = do
  e1 <- gcast e1
  e2 <- gcast e2
  parseSome s (SomeExpr (e1 .+. e2) : stack)

parseSome ('=' : s) (SomeExpr (e1 :: IFix f s1) : SomeExpr (e2 :: IFix f s2) : stack) = do
  Refl <- eqT :: Maybe (s1 :~: s2) 
  parseSome s (SomeExpr (e1 .=. e2) : stack)

parseSome [] [e] = Just e
parseSome _ _ = Nothing

编辑

要解析排序，您需要在类型级别跟踪它们。同样，使用存在类型。

data SomeSort where
  SomeSort :: Typeable (s :: Sort) => proxy s -> SomeSort

你可以这样构建排序数组：

-- \i e -> array i e
arraySort :: SomeSort -> SomeSort -> SomeSort
arraySort (SomeSort (Proxy :: Proxy i)) (SomeSort (Proxy :: Proxy e)) =
  SomeSort (Proxy :: Proxy (ArraySort i e))

这里 Typeable 的一个潜在问题是它只允许你测试类型的相等性，而你可能只想检查头构造函数：你不能问 "is this type an ArraySort?"，但是只有 "is this type equal to ArraySort IntSort BoolSort?" 或其他一些完整类型。在那种情况下，您需要一个反映排序结构的 GADT。

-- "Singleton type"
data SSort (s :: Sort) where
  SIntSort :: SSort IntSort
  SBoolSort :: SSort BoolSort
  SArraySort :: SSort i -> SSort e -> SSort (ArraySort i e)

data SomeSort where
  SomeSort :: SSort s -> SomeSort

array :: SomeSort -> SomeSort -> SomeSort
array (SomeSort i) (SomeSort e) = SomeSort (SArraySort i e)

singleton 包提供了各种用于定义和使用这些单例类型的工具，尽管它对您的用例来说可能有点过分了。

解析索引类型

Parsing an Indexed Type

parsing

haskell

dynamic-typing

dependent-type

编辑