haskell - 在 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

Benjamin Hodgson解释了一个问题在评论中。要解决这个问题，您只需要输入更多类型的 sameSymbol :

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

然后 look可以定义为(假设 weak 被证明):

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

你得到的歧义错误是由于 s在约束中提到，但未在任何地方确定。这很容易修复 — 只需提供 Proxy s :

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

但是在这里我们遇到了一个更难解决的问题。如果一个符号存储在那个 Exp xs a与 s' 相同— 列表中的符号？返回 Var t在这种情况下是不正确的，因为 Var t 的含义改变了:它不再表示列表中间某处的符号——它现在在头部。而且它的类型不正确，因为这需要 a和 b是同一类型。所以这个版本类型检查:

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

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

只需使用 de Bruijn 指数，真的。