【问题标题】:Why doesn't this this instance declaration work in Haskell?为什么这个实例声明在 Haskell 中不起作用?
【发布时间】:2014-03-08 17:48:25
【问题描述】:

我正在尝试创建一个数据类型来表示 Haskell 中的抽象语法树。我一直在阅读有关免费 monad、GADT、混合 Typeable/Dynamic 和其他可能解决此问题的各种内容,但我主要是好奇我提出的解决方案是否可行(即使需要扩展),并且如果没有,为什么不呢?

基本上我有一个类型类:

data AST a b = AST a b
data Atom a = Atom a

class Eval e where
    eval :: e a -> a
instance Eval Atom where
    eval (Atom a) = a

然后对于 AST 的 Eval 实例,我想要类似的东西:

instance Eval (e1 (a -> b)), Eval (e2 a) => Eval (AST b) where
    eval (AST f x) = eval f $ eval x

在英语中,作为Eval b 的实例表示可以将某些东西评估为b,并且我希望AST 成为Eval b 的实例,前提是它的第一个参数可以评估为a -> b它的第二个参数可以评估为a。所以这个想法是 AST 不一定是类型安全的,但如果它不是类型安全的,那么它就不是 Eval 的实例,所以如果你有在非类型安全的 AST 上调用 eval 的代码,它就不会编译。或者甚至只是制作一个像

这样的函数
typecheck :: Eval e => e a -> e a
typecheck = id

作为静态测试。我假设这是不可能的,考虑到我在代表 AST 时看到的所有其他事情,但为什么不是呢?任何扩展都可以使这个基本想法可行吗?我正在做的一个主要要求是我需要能够在运行时生成 AST,将 AST 转换为文本并在之后检查它(所以我显然需要一些 NamedFunction 数据类型),并且我需要能够用它轻松表示任意无点 Haskell 表达式(因此任何可以由一些任意但有限的原始函数/值集构成的东西,但不能使用 let/where/case/lambdas/etc)。

编辑:我觉得问题的一部分是在上述情况下推断 AST 应该是 Eval b 的一个实例。对于Atom,我只是说instance Eval Atom where,但对于AST,如果我有instance ... => Eval AST where,那么我并没有真正说它是Eval b,只是Eval,它不会无论如何都要编译而不给AST添加一个参数,所以问题可能出在某个地方,但我仍然不确定是否没有办法告诉编译器我真正想要的是什么。

【问题讨论】:

  • 忘记e1e2;即使instance (Eval (AST (a -> b)), Eval (AST a)) => Eval (AST b) 也不起作用,因为a 只出现在左边,而不是右边。这对于类型检查器来说是非常有问题的,因为如果您允许这样做,您不能保证实例解析将终止。请参阅UndecideableInstances

标签: haskell


【解决方案1】:

您可以使用TypeFamiliesFlexibleContextsFunctionalDependenciesFlexibleInstancesMultiParamTypeClasses 完成与您在发布的问题中尝试的类似的操作。

TypeFamiliesFunctionalDependencies 都是类型检查器可以完全基于另一种类型来确定一种类型的机制。这将为我们解决两个问题。您遇到的第一个问题是,我们无法在类的实例声明中从类型a->b 中获取类型ab。第二个问题是我们需要能够根据表达式的类型来判断它的计算结果是什么类型。 TypeFamilies 允许我们创建可以解构类型的类型级函数。 FunctionalDependencies 允许我们声明一个类型可以从另一个类型中恢复。

编辑:TypeFamilies 提供了比FunctionalDependencies 更好的解决方案。

类型族

使用TypeFamilies,我们可以从类型中提取出需要的类型

{-#LANGUAGE FlexibleContexts, TypeFamilies, UndecidableInstances #-}
module Main (
    main
) where

data App ef ea = App ef ea
    deriving (Show)

data Atom a = Atom a
    deriving (Show)

class Eval e where
    -- The type of what an expression evaluates to can be determined from the type of the expession
    -- V is a type function that gets this type from the type of the expression
    type V e :: *
    eval :: e -> V e

instance Eval (Atom a) where
    type V (Atom a) = a
    eval (Atom a) = a

-- the class of functions from a to b
-- The only allowed f is (a->b)
-- This creates two type functions, A and B, which can be used to get the type arguments to ->
class (f ~ (A f -> B f)) => F f where
    type A a :: *
    type B b :: *

instance F (a->b) where
    type A (a->b) = a
    type B (a->b) = b

instance (Eval ef, F (V ef), Eval ea, V ea ~ A (V ef)) => Eval (App ef ea) where
    -- B (V ef) is the only thing that requires UndecidableInstances.
    -- It is probably decidable.
    type V (App ef ea) = B (V ef)
    eval (App ef ea) = eval ef $ eval ea

使用需要显式指定多态类型的类型,这不仅是因为单态限制,还因为App (Atom (Integer->Integer)) (Atom Int) 是合法类型,尽管Integer->Integer 不能应用于@ 987654339@.

-- Example code

instance Show (a->b) where
    show _ = "->"

test1 :: (Num n) => App (Atom (n->n)) (Atom n)
test1 = App (Atom (+1)) (Atom 3)

test2 = App (App (Atom ((+) :: Int -> Int -> Int)) (Atom (1 :: Int))) (Atom (3 :: Int))

test3 = App (Atom reverse) (Atom "abc")

main = do
    print test1
    print $ eval test1
    putStrLn ""
    print test2
    print $ eval test2
    putStrLn ""
    print test3
    print $ eval test3

尝试使用不兼容类型的应用程序评估抽象语法树

-- This still type checks
appStringToString = App (Atom "def") (Atom "abc")
-- But this won't
fails = eval appStringToString

编译失败

Couldn't match type `A [Char]' with `[Char]'
In the expression: eval appStringToString
In an equation for `fails': fails = eval appStringToString

编辑: 定义以下内容,并在示例中使用它代替 App,让您在所有示例中放弃所有类型注释。

app :: (Eval ef, F (V ef), Eval ea, V ea ~ A (V ef)) => ef -> ea -> App ef ea
app = App

app 在构造App 时为App 捕获并保留Eval 实例所需的类型信息。用app 构造的表达式树在构造上是正确的。例如

appStringToString = app (Atom "def") (Atom "abc")

导致编译器错误:

Couldn't match type `A [Char]' with `[Char]'
Expected type: A (V (Atom [Char]))
  Actual type: V (Atom [Char])
In the expression: app (Atom "def") (Atom "abc")
In an equation for `appStringToString':
    appStringToString = app (Atom "def") (Atom "abc")

FunctionalDependencies 添加一个类似的函数并不能解决类型推断问题,即使是NoMonomorphismRestriction。这使得TypeFamilies 明显胜过FunctionalDependencies

函数依赖

编辑:TypeFamilies 提供了一个更好的解决方案。此部分仅用于比较。

使用FunctionalDependencies,我们声明该类型可以稍后恢复。它在处理多态性方面不如TypeFamilies

{-#LANGUAGE FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
module Main (
    main
) where

data App ef ea = App ef ea
    deriving (Show)

data Atom a = Atom a
    deriving (Show)

-- Expressions that evaluate to a
-- The type of what an expression evaluates to can be determined from the type of the expession
class Eval a e | e -> a where
    eval :: e -> a

instance Eval a (Atom a) where
    eval (Atom a) = a

-- the class of functions from a to b
class F a b f | f -> a, f -> b where
    func :: f -> (a->b)

instance F a b (a->b) where
    func = id

-- Class of expressions that evaluate to a function a->b
class (Eval f e, F a b f) => EvalF a b f e | e -> f, e -> a, e ->b

-- This requires UndecidaableInstances, but should be decidable
instance (Eval f e, F a b f) => EvalF a b f e

-- This requires UndecidaableInstances, but should be decidable
instance (EvalF a b f ef, Eval a ea) => Eval b (App ef ea) where
    eval (App ef ea) =  func (eval ef) $ eval ea

编译器在对test1求值时无法推断出数字的类型,所以示例需要额外的、繁琐的类型注解:

-- Example code

instance Show (a->b) where
    show _ = "->"

test1 :: (Num n) => App (Atom (n->n)) (Atom n)
test1 = App (Atom (+1)) (Atom 3)

test2 = App (App (Atom ((+) :: Int -> Int -> Int)) (Atom (1 :: Int))) (Atom (3 :: Int))

test3 = App (Atom reverse) (Atom "abc")

main = do
    print test1
    print $ eval (test1 :: App (Atom (Int->Int)) (Atom Int))
    putStrLn ""
    print test2
    print $ eval test2
    putStrLn ""
    print test3
    print $ eval test3

尝试使用不兼容类型的应用程序评估抽象语法树

-- This still type checks
appStringToString = App (Atom "def") (Atom "abc")
-- But this won't
fails = eval appStringToString

编译失败

No instance for (F [Char] a0 [Char]) arising from a use of `eval'
Possible fix: add an instance declaration for (F [Char] a0 [Char])
In the expression: eval appStringToString
In an equation for `fails': fails = eval appStringToString

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 2016-08-18
    • 2022-08-16
    • 1970-01-01
    • 1970-01-01
    • 2021-03-02
    • 2013-10-15
    • 2012-01-12
    相关资源
    最近更新 更多