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.

### Related Questions

#### Sponsored Content

#### 15 Answered Questions

### [SOLVED] Getting started with Haskell

**2009-06-18 13:17:11****anderstornvig****240944**View**755**Score**15**Answer- Tags: haskell functional-programming

#### 8 Answered Questions

### [SOLVED] Large-scale design in Haskell?

**2010-06-20 01:21:10****Dan****57572**View**565**Score**8**Answer- Tags: haskell functional-programming monads large-scale

#### 2 Answered Questions

### [SOLVED] Translate a Scala Type example to Haskell

**2016-12-02 19:21:04****Nigel Benns****368**View**10**Score**2**Answer- Tags: scala haskell types functional-programming

#### 1 Answered Questions

### [SOLVED] Constraints in type family instances

**2016-05-31 16:21:48****prophet-on-that****314**View**8**Score**1**Answer- Tags: haskell type-families

#### 2 Answered Questions

### [SOLVED] Type level environment in Haskell

**2016-05-17 18:08:47****Rodrigo Ribeiro****279**View**2**Score**2**Answer- Tags: haskell dependent-type type-level-computation

#### 1 Answered Questions

### [SOLVED] Techniques for Tracing Constraints

**2014-05-03 18:11:42****crockeea****10150**View**321**Score**1**Answer- Tags: haskell constraints ghc

#### 2 Answered Questions

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

**2015-09-05 22:46:44****Nol****143**View**2**Score**2**Answer- Tags: haskell

#### 1 Answered Questions

### [SOLVED] Weakening vinyl's RecAll constraint through entailment

**2015-04-27 20:17:56****Andrew Thaddeus Martin****386**View**7**Score**1**Answer- Tags: haskell constraints ghc vinyl

#### 1 Answered Questions

#### 1 Answered Questions

### [SOLVED] Debugging compile time performance issues caused by GHC's constraint solver

**2013-07-23 23:11:32****Mike Izbicki****372**View**20**Score**1**Answer- Tags: performance debugging haskell ghc type-constraints

## 1 comments

## @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.

## 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.

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

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!