Trees that grow boilerplate

Learn
#1

Lets say I have data type Expr a as defined in Types

And I have some parser, the details really don’t matter at all here.

The problem arises in my renamer module. The representation for Type is
exactly the same for both modules, yet I need boilerplate to convince the
typechecker. Does there exist some nice way to avoid this?

The problem is exaggerated for modules that modify the tree even less, e.g a desugar module.
I know syb helps with this if the
type of the tree is the same, but that is not the case here.

{-# LANGUAGE TypeFamilies #-}

module Types where

type Pos = (Int, Int)

data Rn
data Ps

data Expr a
    = Var (XVar a) String
    | Lam (XLam a) String (Type a) (Expr a)
    | App (XApp a) (Expr a) (Expr a)

data Type a = Int (XInt a) | Fun (XFun a) (Type a) (Type a)

type family XVar a
type family XLam a
type family XApp a

type family XInt a
type family XFun a

{-# LANGUAGE TypeFamilies #-}

module Parse where
import Types

type instance XVar Ps = Pos
type instance XLam Ps = Pos
type instance XApp Ps = Pos

type instance XInt Ps = ()
type instance XFun Ps = ()

parse :: String -> Expr Ps
parse input = error "todo"

{-# LANGUAGE TypeFamilies #-}

module Rename where

import Types
import Parse ()

type instance XVar Rn = Pos
type instance XLam Rn = Pos
type instance XApp Rn = Pos

type instance XInt Rn = ()
type instance XFun Rn = ()

rename :: Expr Ps -> Expr Rn
rename expr = case expr of
    Lam pos var ty body -> Lam pos var (boilerplate ty) (rename body)
    App pos l r -> App pos (rename l) (rename r)
    Var _ _ -> error "..."

boilerplate :: Type Ps -> Type Rn
boilerplate (Int field) = Int field
boilerplate (Fun field l r) = Fun field (boilerplate l) (boilerplate r)
4 Likes
#2

Presumably it can be polymorphic enough that you need only write it once:

coerceType :: (XInt t1 ~ XInt t2, XFun t1 ~ XFun t2) => Type t1 -> Type t2
1 Like
#3

Thanks! It’s an improvement but not completely satisfying. I suspect not having some coercion function is impossible though.

#4

The closest thing to an “improvement” that I can see for this situation (other than “just use the same type in the first place”) is a bit of unsafe magic:

coercibly
  :: forall t1 t2 r
   . (Coercible (XInt t1) (XInt t2), Coercible (XFun t1) (XFun t2))
  => (Coercible (Type t1) (Type t2) => r) -> r
coercibly r = case magic of Coercion -> r
 where
  magic :: Coercion (Type t1) (Type t2)
  magic = unsafeCoerce refl
   where
    refl :: Coercion (Type t1) (Type t1)
    refl = Coercion

Then you can bring the instance into scope where needed and use safe coercions:

rename :: Expr Ps -> Expr Rn
rename expr = coercibly case expr of
    Lam pos var ty body -> Lam pos var (coerce ty) (rename body)
    App pos l r -> App pos (rename l) (rename r)
    Var _ _ -> error "..."

This avoids traversing the AST to rebuild it unchanged, though GHC optimisations might already be capable of that much.

(use at your own risk)

4 Likes
#5

No, GHC doesn’t recognize what I’ve dubbed “hidden identity functions”.

3 Likes
#6

It’s a pity you can’t use coerce for this!

Ideally you’d be able to mark the parameter to Type as representational phantom, actually!, and that would signal to the compiler to infer a Coercible (Type a) (Type b) from (Coercible (XInt a) (XInt b), Coercible (XFun a) (XFun b)). But the docs say that arguments to type families must be nominal.

I don’t know if the existing roles for type families proposal covers this case exactly, but it seems in the same ballpark.

#7

Extensions to the role system get pretty complicated. For cases like this, I think it would be plenty to partially lift the restriction on user-declared Coercible instances: let us standalone-derive them, with GHC throwing a compile error if it can’t prove representational equality from the constraints we supply.

#8

I’d simply go for an unsafeCoerce-based solution such as @Leary’s. The pass parameter can’t really be phantom, because it is used in type families. besides, a coercebased solution is unlikely to be better than one based on unsafeCoerce if you know what you are doing. That is, if you think you should be allowed to use coerce, you can always use unsafeCoerce as well.

1 Like