By Andrew Thaddeus Martin

2015-09-09 13:50:58 8 Comments

I'm playing around with the constraints package (for GHC Haskell). I have a type family for determining if a type-level list contains an element:

type family HasElem (x :: k) (xs :: [k]) where
  HasElem x '[] = False                                                                               
  HasElem x (x ': xs) = True                                                                          
  HasElem x (y ': xs) = HasElem x xs

This works, but one thing it doesn't give me is the knowledge that

HasElem x xs   entails   HasElem x (y ': xs)

since the type family isn't an inductive definition of the "is element of" statement (like you would have in agda). I'm pretty sure that, until GADTs are promotable to the type level, there is no way to express list membership with a data type.

So, I've used the constraints package to write this:

containerEntailsLarger :: Proxy x -> Proxy xs -> Proxy b -> (HasElem x xs ~ True) :- (HasElem x (b ': xs) ~ True)
containerEntailsLarger _ _ _ = unsafeCoerceConstraint

Spooky, but it works. I can pattern match on the entailment to get what I need. What I'm wondering is if it can ever cause a program to crash. It seems like it couldn't, since unsafeCoerceConstraint is defined as:

unsafeCoerceConstraint = unsafeCoerce refl

And in GHC, the type level is elided at runtime. I thought I'd check though, just to make sure that doing this is ok.

--- EDIT ---

Since no one has given an explanation yet, I thought I would expand the question a little. In the unsafe entailment I'm creating, I only expect a type family. If I did something that involved typeclass dictionaries instead like this:

badEntailment :: Proxy a -> (Show a) :- (Ord a)
badEntailment _ = unsafeCoerceConstraint

I assume that this would almost certainly be capable of causing a segfault. Is this true? and if so, what makes it different from the original?

--- EDIT 2 ---

I just wanted to provide a little background for why I am interested in this. One of my interests is making a usable encoding of relational algebra in Haskell. I think that no matter how you define functions to work on type-level lists, there will be obvious things that aren't proved correctly. For example, a constraint (for semijoin) that I've had before looked like this (this is from memory, so it might not be exact):

semijoin :: ( GetOverlap as bs ~ Overlap inAs inBoth inBs
            , HasElem x as, HasElem x (inAs ++ inBoth ++ inBs)) => ...

So, it should be obvious (to a person) that if I take union of two sets, that it contains an element x that was in as, but I'm not sure that it's possible the legitimately convince the constraint solver of this. So, that's my motivation for doing this trick. I create entailments to cheat the constraint solver, but I don't know if it's actually safe.


@dfeuer 2015-09-09 20:03:33

I don't know if this will suit your other needs, but it accomplishes this particular purpose. I'm not too good with type families myself, so it's not clear to me what your type family can actually be used for.

{-# LANGUAGE ...., UndecidableInstances #-}
type family Or (x :: Bool) (y :: Bool) :: Bool where
  Or 'True x = 'True
  Or x 'True = 'True
  Or x y = 'False

type family Is (x :: k) (y :: k) where
  Is x x = 'True
  Is x y = 'False

type family HasElem (x :: k) (xs :: [k]) :: Bool where
  HasElem x '[] = 'False
  HasElem x (y ': z) = Or (Is x y) (HasElem x z)

containerEntailsLarger :: proxy1 x -> proxy2 xs -> proxy3 b ->
                          (HasElem x xs ~ 'True) :- (HasElem x (b ': xs) ~ 'True)
containerEntailsLarger _p1 _p2 _p3 = Sub Dict

An approach using GADTs

I've been having trouble letting go of this problem. Here's a way to use a GADT to get good evidence while using type families and classes to get a good interface.

-- Lots of extensions; I don't think I use ScopedTypeVariables,
-- but I include it as a matter of principle to avoid getting
-- confused.
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

-- Some natural numbers
data Nat = Z | S Nat deriving (Eq, Ord, Show)

-- Evidence that a type is in a list of types
data ElemG :: k -> [k] -> * where
  Here :: ElemG x (x ': xs)
  There :: ElemG x xs -> ElemG x (y ': xs)
deriving instance Show (ElemG x xs)

-- Take `ElemG` to the class level.
class ElemGC (x :: k) (xs :: [k]) where
  elemG :: proxy1 x -> proxy2 xs -> ElemG x xs

-- There doesn't seem to be a way to instantiate ElemGC
-- directly without overlap, but we can do it via another class.
instance ElemGC' n x xs => ElemGC x xs where
  elemG = elemG'

type family First (x :: k) (xs :: [k]) :: Nat where
  First x (x ': xs) = 'Z
  First x (y ': ys) = 'S (First x ys)

class First x xs ~ n => ElemGC' (n :: Nat) (x :: k) (xs :: [k]) where
  elemG' :: proxy1 x -> proxy2 xs -> ElemG x xs

instance ElemGC' 'Z x (x ': xs) where
  elemG' _p1 _p2 = Here

instance (ElemGC' n x ys, First x (y ': ys) ~ 'S n) => ElemGC' ('S n) x (y ': ys) where
  elemG' p1 _p2 = There (elemG' p1 Proxy)

This actually seems to work, at least in simple cases:

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Int, Char])

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Int, Int])
There Here

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Integer, Int])
There (There Here)

This doesn't support the precise entailment you desire, but I believe the ElemGC' recursive case is probably the closest you can get with such an informative constraint, at least in GHC 7.10.

@Andrew Thaddeus Martin 2015-09-09 22:42:30

Cool approach. This very neatly sidesteps the issue I was running into. I will update my question to explain more about the motivation for this.

@Edward KMETT 2015-09-09 23:48:45

This is definitely the right approach for this problem.

@dfeuer 2015-09-10 19:15:07

Thanks, @EdwardKMETT. What do you think of the GADT approach I added? Is there a better way to do that? I'm not a big fan of the First x (y ': ys) ~ Just (S n) constraint, since it doesn't build on First x ys ~ Just n, but I don't see a way around it as yet.

@Andrew Thaddeus Martin 2015-09-11 12:22:53

Nice. I read the hasochism paper very recently, so this is a good example for me to see. Just to make sure that I correctly understand, is the class ElemGC (which isn't used in your GHCi example) used to implicitly create an ElemG (like what NATTY is in the hasochism paper)?

@dfeuer 2015-09-11 12:35:06

@AndrewThaddeusMartin, it is used in the example! I used the elemG function. Yes, it implicitly creates an ElemG. I've not read the paper yet, but I guess I should.

@Andrew Thaddeus Martin 2015-09-11 16:13:35

@dfeuer Ah, indeed it is used! Sorry I missed that.

@Edward KMETT 2015-09-15 02:09:10

If you want to avoid closed type families you can use overlapping instances: instance {-# OVERLAPPABLE #-} ElemGC x (x ': xs) where elemG _ _ = Here; instance {-# OVERLAPS #-} ElemGC x ys => ElemGC x (y ': ys) where elemG p _ = There (elemG p (Proxy :: Proxy ys));

@dfeuer 2015-09-15 02:55:38

@EdwardKMETT, I finally realized just now how the new OVERLAPS and OVERLAPPABLE improve over the old OverlappingInstances for this. Thanks!

Related Questions

Sponsored Content

2 Answered Questions

[SOLVED] Techniques for Tracing Constraints

15 Answered Questions

[SOLVED] Getting started with Haskell

2 Answered Questions

[SOLVED] Translate a Scala Type example to Haskell

1 Answered Questions

[SOLVED] Constraints in type family instances

2 Answered Questions

[SOLVED] Type level environment in Haskell

2 Answered Questions

[SOLVED] Constrain elements of a type-level list in Haskell

  • 2015-09-05 22:46:44
  • Nol
  • 166 View
  • 2 Score
  • 2 Answer
  • Tags:   haskell

1 Answered Questions

[SOLVED] Weakening vinyl's RecAll constraint through entailment

1 Answered Questions

[SOLVED] Circular Typing with Constraints

  • 2014-11-24 04:30:21
  • crockeea
  • 179 View
  • 2 Score
  • 1 Answer
  • Tags:   haskell ghc

1 Answered Questions

Sponsored Content