haskell TypeNats与定制数据语句的问题

6tr1vspr  于 2022-11-14  发布在  其他
关注(0)|答案(2)|浏览(161)

我一直在为一个简单的表达式语言尝试一个赋值函数,主要是为了熟悉一些我以前没有用过的Haskell扩展。最新的实验是使用DataKinds和TypeFamilies来统一一元和二元运算符。经过一些麻烦之后,我使它工作了,但前提是我用一个定制的自然数定义来表示运算符的arity:

data NatT = ZeroT | SuccT NatT

如果我尝试使用TypeNats,编译器将无法匹配类型。下面是失败的版本。这是apply函数的第二行,编译器对此感到不满-fa的应用程序。错误是无法将Double -> FuncN (n - 1)FuncN n匹配。(这正好是FuncN定义的第二行)。我使用n+1n代替nn-1会得到不同的错误。我还尝试将FuncN声明为单射的,但编译器也不喜欢这样。
这个问题并没有让我感到惊讶,我对使用NatT的工作版本感到满意,但我有兴趣看看是否有可能在使用TypeNats的同时解决这个问题。

{-#LANGUAGE FlexibleInstances, GADTs, DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

module FourFours
    ( NularyOp(..)
    , UnaryOp(..)
    , BinaryOp(..)
    , Term(..)
    , ListN(..)
    , eval
    ) where

import GHC.TypeNats

type family FuncN n where
    FuncN 0 = Double
    FuncN n = Double -> FuncN (n - 1)

data ListN n a where
    EmptyN :: ListN 0 a
    ConsN :: a -> ListN (n - 1) a -> ListN n a

instance Functor (ListN n) where
    fmap f EmptyN = EmptyN
    fmap f (ConsN a as) = ConsN (f a) (fmap f as)

apply :: FuncN n -> ListN n Double -> Double
apply x EmptyN = x
apply f (ConsN x xs) = apply (f x) xs

data NularyOp = Four | FortyFour | PointFour   deriving (Eq, Ord, Enum)
data UnaryOp = Sqrt                            deriving (Eq, Ord, Enum)
data BinaryOp = Add | Sub | Mul | Div | Pow    deriving (Eq, Ord, Enum)

class Op o where
    type Arity o :: Nat
    evalOp :: o -> FuncN (Arity o)

instance Op NularyOp where
    type Arity NularyOp = 0
    evalOp Four = 4
    evalOp FortyFour = 44
    evalOp PointFour = 0.4

instance Op UnaryOp where
    type Arity UnaryOp = 1
    evalOp Sqrt = sqrt

instance Op BinaryOp where
    type Arity BinaryOp = 2
    evalOp Add = (+)
    evalOp Sub = (-)
    evalOp Mul = (*)
    evalOp Div = (/)
    evalOp Pow = (**)

data Term n where
    OpTerm :: Op o => o -> Term (Arity o)
    Apply :: Term n -> ListN n (Term 0) -> Term 0

eval :: Term n -> FuncN n
eval (OpTerm o) = evalOp o
eval (Apply o ts) = apply (eval o) (fmap eval ts)
tktrz96b

tktrz96b1#

这里有一个解决这个问题的方法。这个方法有点局限--在这种情况下适用,因为所讨论的特定程序只使用了Nat中的几个类型。它也是低效的。但它至少避免了使用像unsafeCoerceOverlappingInstances这样的讨厌的东西。
GHC的困难在于处理FuncN类型族。要对apply函数的ConsN子句的右侧进行类型检查,GHC需要推导出FuncN (n + 1) ~ Double -> FuncN n。当特定类型(012...)替代了n,但无法推导出具有类型变量n的一般形式。
您可以考虑使用FuncN (n + 1) = Double -> FuncN n作为FuncN定义的第二个子句,但这是不允许的,因为操作符(+)不是构造函数:这是一个类型族,即使可以这样做,我也不认为会有什么帮助,因为GHC甚至不能排除FuncN的第一个子句适用于n + 1的可能性.
解决这个问题的技巧是生成类型相等的证据,以命题相等项FuncN (n + 1) :~: Double -> FuncN n的形式。我们为函数定义了一个类型别名,该函数将Nat中特定类型的代理Map到相应的证据上。

type FuncNProp n = Typeable n => Proxy n -> (FuncN (n + 1) :~: (Double -> FuncN n))

我们需要Typeable约束,这样才能使用eqT
我还没有找到构造这种类型的全函数的方法,但这里有一个只包含01的方法,这是我们在这个特定程序中唯一需要的。

funcNProp :: forall n . FuncNProp n
funcNProp (proxy :: Proxy n) = case eqT @n @0
                                    of Just Refl -> Refl
                                       Nothing -> case eqT @n @1
                                                       of Just Refl -> Refl
                                                          Nothing -> error "Operators with arity greater than 2 not supported"

eqT测试允许GHC分别考虑01情况。返回的Refl值是GHC可以进行类型检查的证据,因为它可以推导出Nat中特定的单个类型的FuncN (n + 1) ~ Double -> FuncN n
然后,我们更新apply的第二个子句,以使用此证据

apply f (ConsN x (xs :: ListN n' Double)) = case funcNProp (Proxy :: Proxy n' ) of Refl -> apply (f x) xs

...在ConsN模式子句中,我们还将n'与该类型匹配。使用该类型,我们构造一个代理传递给funcNProp,该代理生成对apply (f x) xs进行类型检查所需的证据。
以下是完整的计划:

{-#LANGUAGE FlexibleInstances
          , GADTs
          , DataKinds
          , TypeFamilies
          , TypeOperators
          , UndecidableInstances
          , ScopedTypeVariables
          , RankNTypes
          , TypeApplications
          , FlexibleContexts #-}

module FourFours
    ( NularyOp(..)
    , UnaryOp(..)
    , BinaryOp(..)
    , Term(..)
    , ListN(..)
    , eval
    ) where

import GHC.TypeNats ( Nat, type (+), type (-) )
import Data.Typeable ( Typeable, Proxy(..), type (:~:)(..), eqT )

type family FuncN n where
    FuncN 0 = Double
    FuncN n = Double -> FuncN (n - 1)

data ListN n a where
    EmptyN :: ListN 0 a
    ConsN :: Typeable n => a -> ListN n a -> ListN (n + 1) a

instance Functor (ListN n) where
    fmap f EmptyN = EmptyN
    fmap f (ConsN a as) = ConsN (f a) (fmap f as)

type FuncNProp n = Typeable n => Proxy n -> (FuncN (n + 1) :~: (Double -> FuncN n))

funcNProp :: forall n . FuncNProp n
funcNProp (proxy :: Proxy n) = case eqT @n @0
                                    of Just Refl -> Refl
                                       Nothing -> case eqT @n @1
                                                       of Just Refl -> Refl
                                                          Nothing -> error "Operators with arity greater than 2 not supported"

apply :: forall n . FuncN n -> ListN n Double -> Double
apply x EmptyN = x
apply f (ConsN x (xs :: ListN n' Double)) = case funcNProp (Proxy :: Proxy n' ) of Refl -> apply (f x) xs

data NularyOp = Four | FortyFour | PointFour   deriving (Eq, Ord, Enum)
data UnaryOp = Sqrt                            deriving (Eq, Ord, Enum)
data BinaryOp = Add | Sub | Mul | Div | Pow    deriving (Eq, Ord, Enum)

class Op o where
    type Arity o :: Nat
    evalOp :: o -> FuncN (Arity o)

instance Op NularyOp where
    type Arity NularyOp = 0
    evalOp Four = 4
    evalOp FortyFour = 44
    evalOp PointFour = 0.4

instance Op UnaryOp where
    type Arity UnaryOp = 1
    evalOp Sqrt = sqrt

instance Op BinaryOp where
    type Arity BinaryOp = 2
    evalOp Add = (+)
    evalOp Sub = (-)
    evalOp Mul = (*)
    evalOp Div = (/)
    evalOp Pow = (**)

data Term n where
    OpTerm :: Op o => o -> Term (Arity o)
    Apply :: Term n -> ListN n (Term 0) -> Term 0

eval :: Term n -> FuncN n
eval (OpTerm o) = evalOp o
eval (Apply o ts) = apply (eval o) (fmap eval ts)
31moq8wy

31moq8wy2#

事实证明,还有另一种解决方案,只需添加一个仔细放置的约束。
如前所述,GHC的难点在于处理FuncN类型族。要对apply函数的ConsN子句的右侧进行类型检查,GHC需要推导出FuncN (n + 1) ~ Double -> FuncN n。当特定类型(012 ...)替代了n,但无法用类型变量n推导出一般形式。
解决方案是将该约束添加到ListN数据定义的ConsN子句中。也就是说,实际上,只承诺构造满足该属性的列表。由于该属性是一个同义反复,因此这不是一个限制,但是,更重要的是,如果所有ListN构造都是文字的(因此TypeNat是特定示例),GHC能够建立该属性,这是该特定程序的情况。
整个程序:

{-#LANGUAGE GADTs
          , DataKinds
          , TypeFamilies
          , TypeOperators
          , UndecidableInstances #-}

module Main where

import GHC.TypeNats ( Nat, type (+), type (-) )

type family FuncN n where
    FuncN 0 = Double
    FuncN n = Double -> FuncN (n - 1)

data ListN n a where
    EmptyN :: ListN 0 a
    ConsN :: FuncN (n + 1) ~ (Double -> FuncN n) => a -> ListN n a -> ListN (n + 1) a

instance Functor (ListN n) where
    fmap f EmptyN = EmptyN
    fmap f (ConsN a as) = ConsN (f a) (fmap f as)

apply :: FuncN n -> ListN n Double -> Double
apply x EmptyN = x
apply f (ConsN x xs) = apply (f x) xs

data NularyOp = Four | FortyFour | PointFour   deriving (Eq, Ord, Enum)
data UnaryOp = Sqrt                            deriving (Eq, Ord, Enum)
data BinaryOp = Add | Sub | Mul | Div | Pow    deriving (Eq, Ord, Enum)

class Op o where
    type Arity o :: Nat
    evalOp :: o -> FuncN (Arity o)

instance Op NularyOp where
    type Arity NularyOp = 0
    evalOp Four = 4
    evalOp FortyFour = 44
    evalOp PointFour = 0.4

instance Op UnaryOp where
    type Arity UnaryOp = 1
    evalOp Sqrt = sqrt

instance Op BinaryOp where
    type Arity BinaryOp = 2
    evalOp Add = (+)
    evalOp Sub = (-)
    evalOp Mul = (*)
    evalOp Div = (/)
    evalOp Pow = (**)

data Term n where
    OpTerm :: Op o => o -> Term (Arity o)
    Apply :: Term n -> ListN n (Term 0) -> Term 0

eval :: Term n -> FuncN n
eval (OpTerm o) = evalOp o
eval (Apply o ts) = apply (eval o) (fmap eval ts)

main :: IO ()
main = let subterm = Apply (OpTerm Sqrt) (ConsN (OpTerm Four) EmptyN)
           term = Apply (OpTerm Add) (ConsN subterm (ConsN (OpTerm Four) EmptyN))
       in print $ eval term

相关问题