Proof of a fairly simple theorem in Haskell

Question

I try, without success, to experiment with add-on programming in Haskell. My idea is to express some weakening property on finite mappings. All 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 lr = l If 'False lr = 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 ss' of Just Refl -> p Nothing -> look s rho 

The GHC complains that the look s rho call is not of type Exp xs a , since the recursive call is made in the final rho environment with fewer entries than the original. I believe the solution is to weaken Exp xs a to Exp ('(s,b) ': xs) a . Here is my attempt to weaken the 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 the GHC responds with an ambiguity error like:

 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 know that such easing can be easily implemented if we use De Bruijn typed indices to represent variables. My question is: is it possible to implement it for names instead of indexes? If so, how can this be done?

Answer 1

One of the problems is explained by Benjamin Hodgson in the comments. To do this, you just need to type the sameSymbol :

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

Then look can be defined as (assuming weak 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 ss' of Left Refl -> weak s $ look s rho Right Refl -> p 

The ambiguity error you get is related to the fact that s is mentioned in the constraints, but not defined anywhere. This is easy to fix - just specify Proxy s :

 weak :: forall ss' 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 are faced with a problem that is much more difficult to fix. What if the character stored in this Exp xs a matches the character s' , the character preceding the list? The return of Var t would be incorrect in this case, because the value of Var t was changed: it no longer denotes a symbol somewhere in the middle of the list - now it is in the head. And it does not print correctly, because it requires a and b be of the same type. Thus, this type of version checks:

 weak :: forall ss' 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 the stored character cannot be s' , because this situation is explicitly refuted by defining look " - you can say. Good luck to prove it.

Just use the Bruijn indexes, really.