Proving a rather simple theorem in Haskell

Question

I'm trying, without success, some experiments with dependently typed programming in Haskell. My idea is to express some sort of weakening property on finite mappings. The whole code is as follows:

{-# 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 complains that call look s rho doesn't have type Exp xs a, since recursive call is done on a finite environment rho with less entries than the original one. I believe that the solution is to weaken Exp xs a to Exp ('(s,b) ': xs) a. Here goes my try to weaken expressions:

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)

and GHC responds with a type ambiguity error:

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

I'm aware that such weakening can be easily implemented if we use typed De Bruijn indexes to represent variables. My question is: Is possible to implement it for names instead of indexes? If so, how it can be done?

Answer 1

One problem is explained by Benjamin Hodgson in the comments. For this to solve you just need a more typed 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'

Then look can be defined as (assuming weak is proved):

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

The ambiguity error you get is due to the fact that s is mentioned in the constraints, but is not determined anywhere. This is easy to fix — just provide a 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) = ...

But here we encounter a problem that is much harder to fix. What if a symbol stored in that Exp xs a is the same as s' — the symbol prepended to the list? Returning Var t would be incorrect in this case, because the meaning of Var t is changed: it no longer denotes a symbol somewhere in the middle of the list — it's in the head now. And it's not type correct, since that requires a and b to be the same type. So this version type checks:

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')

but the one you desire does not. "But we know that a stored symbol cannot be s', because this situation is explicitly refuted by the way look is defined" — you might say. Good luck proving it.

Just use de Bruijn indices, really.