Make strong typing

In the following pseudo code,

data A = A   
data B = B
data C = C

f1 :: A | B -> IO ()
f1 = undefined

f2 :: A | C -> IO ()
f2 = undefined

I need the compiler to ensure that f1 only accepts types A or B , and f2 accepts types A or C . Any attempt to pass type C to f1 should be caught during compile time, not runtime. I’m currently seeking guidance on how to achieve this. Any help would be appreciated. Thank you!

I do not recommend actually using this everywhere. Type classes are hard to get right, but you can use them to do it:

class F1 a where
  f1 :: a -> IO ()

instance F1 A where
  f1 = undefined
instance F1 B where
  f1 = undefined

class F2 a where
  f2 :: a -> IO ()

instance F2 A where
  f2 = undefined
instance F2 C where
  f2 = undefined
3 Likes

You can go with type class polymorphims as @jaror posted, but I’d say the easiest approach is to use Either

f1 :: Either A B -> IO ()
f2 :: Either A C -> IO ()

Maybe, you don’t want to do this because you don’t want to tag your A's, Bs and C's with Left and Right.

Iit is difficult to tell with no more knowledge about your use case. For example, if A works as a “parent class”. other approach would be to use a polymorphic A

-- Example
data A inner = A { payload1: String, payload2: inner }
data B = ...
data C = ...

-- this means "use A and B", instead of "Use A or B"
f1 :: A B - > IO ()
f1 :: A C -> IO ()

4 Likes

What is the actual problem you’re trying to solve in this particular way? If you can provide more information of your particular scenario, we can probably give a better answer.

Hello everyone, thanks for volunteering to help with my question.

Initially, I aimed to implement strong typing in my library. Golang provides excellent thread communication via goroutines, utilizing channels in three forms:

  1. ch chan: Sendable and receivable
  2. ch <-chan: Only receivable
  3. ch chan<-: Only sendable

However, due to some boring Golang background, I had to omit this original goal and focused on a more concise issue as outlined in the question post.

Nonetheless, I found a workaround by referencing @jaror’s answer. Thanks!

4 Likes

Glad your problem was resolved.

If you’re into well-typed multithreaded communication, you might want to take a look at HasChor! :blush:

4 Likes

Since the title brings up strong typing, I can’t help but notice:

Using Either is stronger because it is more closed.

Using classes is weaker because it is more open.

So there is some irony in asking “how to make it stronger?” and then cheerfully concluding that the weaker approach is preferred.

1 Like

Openness doesn’t detract from strength here. Both solutions result in programs in which the compiler can guarantee that functions will be called only with arguments having the types the function expects.

1 Like

Is there even a rigid definition of “strong typing”?

1 Like

But “stronger” comparing two approaches is pretty unambiguous.

OP seems satisfied with the answer, if you want to further discuss types please open a new thread.

I’d like to throw in one thing though: Either works fine here, but it’s a bit unexpressive in much the same way Bool is (a.k.a. “Boolean Blindness” - you might call this “Either Blindness”).

In a nutshell, Either is the “meaningless sum type”, in the same way that Bool is the “meaningless binary type” - just like True by itself doesn’t mean anything, neither does Left A on its own.

The recommendation for Bool is to either get rid of the binary type altogether and embed the yes/no information in the structure of the code itself (e.g. by pattern matching on the tested data structures directly), or to introduce a specialized binary type that captures the actual situation (e.g. data Result = Success | Failure, which, unlike Bool, doesn’t suffer from the problem of telling whether True means “yes, the operation was successful”, or “yes, the operation failed”).

And so I’d be inclined to introduce custom sum types for these cases here:

data F1 = F1A A | F1B B

f1 :: F1 -> IO ()
f1 (F1A a) = undefined
f1 (F1B b) = undefined

The downside of this is that you don’t get the Functor, Applicative, Monad, etc., instances from Either for free, and the above is maybe not the most illustrative example, but personally, I think it’s worth considering - especially when you need to cater for more than two possible types.


Oh, and there’s a third option, which is to move the typeclass machinery to the type level. It doesn’t always make sense, but the idea is this:

Given the typeclass approach @jaror proposed:

class F1 a where
  f1 :: a -> IO ()

instance F1 A where
  f1 = implementF1ForA
instance F1 B where
  f1 = implementF1ForB

…we can consider a typeclass instance a mapping of a type (e.g. A) to a method dictionary (e.g. f1 -> implementF1ForA). And that is actually how instances work behind the scenes (unless the compiler optimizes them away, that is) - a hidden reference to a typeclass dictionary is passed around with each polymorphic function call, telling the compiler which instance to use.

And now the trick is that we can just do this explicitly, and get rid of the typeclass:

newtype F1 a = F1 { f1Impl :: a -> IO () }

f1A :: F1 a
f1A = F1 { f1Impl = implementF1ForA }

f1B :: F1 b
f1B = F1 { f1Impl = implementF1ForB }

-- and now we can write a polymorphic f1 without using typeclasses:

f1 :: F1 a -> a -> IO ()
f1 impl a = f1impl impl a

This all looks a bit silly in isolation, but in practice, when writing the kind of code you would normally use typeclasses for, it provides another potentially useful point in the design space. Specifically, it maintains the openness of typeclasses, and the decoupling that allows them to act as abstraction boundaries, but it solves some of the pesky dependency issues that typeclasses are riddled with, most importantly the orphan problem. That’s because we are explicit about the “instance”, and having multiple “instances” for the same combination of type and typeclass is no problem (we can have as many values of type F1 A as we want, each doing a different thing, we just need to make sure we pass the one we want to f1).

The downside is of course that you have to pass your “instances” around explicitly, which can lead to visual clutter.


And I just thought of a fourth solution. If what you really want is just to tag your channels as “read-only”, “read-write”, or “write-only”, you could go crazy with type-level programming and do something like this (imports omitted for brevity, requires the DataKinds extension, and probably a few more, and entirely untested):

data Readable = Readable | NotReadable
data Writeable = Writeable | NotWriteable

newtype TypedChan (r :: Readable) (w :: Writeable) a = TypedChan (Chan a)

readTypedChan :: TypedChan Readable w a -> IO a
readTypedChan (TypedChan chan) = readChan chan

writeTypedChan :: TypedChan r Writeable a -> a -> IO ()
writeTypedChan (TypedChan chan) = writeChan chan

newTypedChanReadonly :: IO (TypedChan Readable NotWritable a)
newTypedChanReadonly = TypedChan <$> newChan

newTypedChanWriteonly :: IO (TypedChan NotReadable Writable a)
newTypedChanWriteonly = TypedChan <$> newChan

newTypedChanDuplex :: IO (TypedChan Readable Writable a)
newTypedChanDuplex = TypedChan <$> newChan

The idea here is that we track “readability” and “writeability” at the type level, using phantom types (defined as data types, which is why we need DataKinds). Think of data Readability = Readable | NotReadable as a kind definition that introduces the kind Readability, and two types, Readable and NotReadable, both of kind Readability. Neither Readable nor NotReadable is inhabited by any values, and you cannot use them like “normal” Haskell types, because they are not of kind Type, but the type checker can still use and check them just fine, and that’s what we’re exploiting here: writeTypedChan accepts any readability (r), but requires that the writeability is Writeable - if it’s not, then the code will not type check. And similarly for readTypedChan. And then our channel construction functions (newTypedChan...) allow us to construct types that are tagged with the appropriate readability and writeability types.

4 Likes

Great! The code beautifully harnesses Haskell’s power. Learend what phantom type is and how it can be exploited. Thank you!

I made some slight modifications to your code to make it work, but as I don’t have permission to alter your original response, could you please update the code to ensure it is fully functional?

{-# LANGUAGE KindSignatures, DataKinds #-}

import Control.Concurrent.Chan

data ReadC = Readable | NotReadable
data WriteC = Writable | NotWritable

newtype TypedChan (r :: ReadC) (w :: WriteC) a = TypedChan (Chan a)

readTypedChan :: TypedChan Readable w a -> IO a
readTypedChan (TypedChan chan) = readChan chan

writeTypedChan :: TypedChan r Writable a -> a -> IO ()
writeTypedChan (TypedChan chan) = writeChan chan

newTypedChanReadonly :: IO (TypedChan Readable NotWritable a)
newTypedChanReadonly = TypedChan <$> newChan

newTypedChanWriteonly :: IO (TypedChan NotReadable Writable a)
newTypedChanWriteonly = TypedChan <$> newChan

newTypedChanDuplex :: IO (TypedChan Readable Writable a)
newTypedChanDuplex = TypedChan <$> newChan
1 Like

I don’t think I can edit messages, at least there doesn’t seem to be a button for it or anything, and the “e” keyboard shortcut doesn’t seem to do anything.

I don’t think I can edit messages […]

You’re able to edit your own messages by clicking on the pencil icon:

image

at the end of the post.

1 Like