在Haskell中证明一个相当简单的定理

Question

我正在尝试在Haskell中使用依赖类型编程的一些实验,但没有成功.我的想法是在有限映射上表达某种弱化属性.整个代码如下:

{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE ScopedTypeVariables      #-}

module Exp where

import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits

 data Exp (env :: [(Symbol,*)]) (a :: *) where
   Val :: Int -> Exp env Int
   Var :: (KnownSymbol s, Lookup s env ~ 'Just a) => Proxy s -> Exp env a

 data HList (xs :: [(Symbol,*)]) where
    Nil :: HList '[]
    (:*) :: KnownSymbol s => (Proxy s, Exp ('(s,a) ': xs) a) -> HList xs -> HList ('(s,a) ': xs)

 infixr 5 :*

 type family If (b :: Bool) (l :: k) (r :: k) :: k where
    If 'True  l r = l
    If 'False l r = r

 type family Lookup (s :: Symbol) (env :: [(Symbol,*)]) :: Maybe * where
    Lookup s '[]             = 'Nothing
    Lookup s ('(t,a) ': env) = If (s == t) ('Just a) (Lookup s env)

 look :: (Lookup s xs ~ 'Just a, KnownSymbol s) => Proxy s -> HList xs -> Exp xs a
 look s ((s',p) :* rho) = case sameSymbol s s' of
                            Just Refl -> p
                            Nothing   -> look s rho

GHC抱怨调用look s rho没有类型Exp xs a,因为递归调用是在有限环境下完成的,其rho条目少于原始调用.我相信解决方案是削弱Exp xs a到Exp ('(s,b) ': xs) a.这是我试图削弱表达式:

weak :: (Lookup s xs ~ 'Just a
        , KnownSymbol s
        , KnownSymbol s'
        , (s == s') ~ 'False) => Exp xs a -> Exp ('(s', b) ': xs) a
weak (Val n) = Val n
weak (Var s) = Var (Proxy :: Lookup s ('(s', b) ': xs) ~ 'Just a => Proxy s)

和GHC响应类型歧义错误:

Could not deduce: Lookup s0 xs ~ 'Just a
  from the context: (Lookup s xs ~ 'Just a,
                     KnownSymbol s,
                     KnownSymbol s',
                     (s == s') ~ 'False)
    bound by the type signature for:
               weak :: (Lookup s xs ~ 'Just a, KnownSymbol s, KnownSymbol s',
                        (s == s') ~ 'False) =>
                       Exp xs a -> Exp ('(s', b) : xs) a

我知道如果我们使用类型化的De Bruijn索引来表示变量,那么这种弱化可以很容易地实现.我的问题是:是否可以为名称而不是索引实现它？如果是这样,怎么办？

Answer 1

本杰明·霍奇森在评论中解释了一个问题。为了解决这个问题，你只需要一个更多的类型sameSymbol：

\n\n

sameOrNotSymbol :: (KnownSymbol a, KnownSymbol b)\n                => Proxy a -> Proxy b -> Either ((a == b) :~: \'False) (a :~: b)\nsameOrNotSymbol s s\' = maybe (Left $ unsafeCoerce Refl) Right $ sameSymbol s s\'\n

\n\n

那么look可以定义为（假设weak被证明）：

\n\n

look :: (Lookup s xs ~ \'Just a, KnownSymbol s)\n     => Proxy s -> HList xs -> Exp (DropWhileNotSame (s, a) xs) a\nlook s ((s\',p) :* rho) = case sameOrNotSymbol s s\' of\n  Left  Refl -> weak s $ look s rho\n  Right Refl -> p\n

\n\n

s您得到的歧义错误是由于约束中提到的事实造成的，但在任何地方都没有确定。这很容易修复 \xe2\x80\x94 只需提供Proxy s：

\n\n

weak :: forall s s\' xs a b. (KnownSymbol s\n        , KnownSymbol s\'\n        , (s == s\') ~ \'False)\n     => Proxy s -> Exp xs a -> Exp (\'(s\', b) \': xs) a\nweak s (Val n) = Val n\nweak s (Var t) = ...\n

\n\n

但在这里我们遇到了一个更难解决的问题。如果其中存储的符号与列表前面的符号 \xe2\x80\x94Exp xs a相同怎么办？s\'在这种情况下，返回Var t将是不正确的，因为 的含义Var t已更改：它不再表示列表 \xe2\x80\x94 中间某处的符号，它现在位于头部。而且它的类型不正确，因为这需要a和b是相同的类型。所以这个版本类型检查：

\n\n

weak :: forall s s\' xs a a. (KnownSymbol s\n        , KnownSymbol s\'\n        , (s == s\') ~ \'False)\n     => Proxy s -> Exp xs a -> Exp (\'(s\', a) \': xs) a\nweak s (Val n) = Val n\nweak s (Var t) = case sameOrNotSymbol t (Proxy :: Proxy s\') of\n  Left  Refl -> Var t\n  Right Refl -> Var (Proxy :: Proxy s\')\n

\n\n

但你想要的却没有。“但我们知道存储的符号不能是s\'，因为这种情况已被定义的方式明确反驳look” \xe2\x80\x94 你可能会说。祝你好运，证明这一点。

\n\n

实际上，只需使用 de Bruijn 指数即可。

\n