In Kotlin i can do

sealed class Substance {
    object Uranus : Substance()
    object Mercury: Substance()
    object Ammonia : Substance()
}

data class DangerousBox<T : Substance>(val item: T)

fun main() {
    val uranus = DangerousBox<Substance.Uranus>(Substance.Uranus)
    val mercury: DangerousBox<Substance.Mercury> = uranus
}

Now i have invariant types DangerousBox<Substance.Uranus>, DangerousBox<Substance.Mercury> etc., so sample above would't compile.

How make it in Haskell?

Ideally i would like to have types

uranus :: DangerousBox Uranus
uranus = DangerousBox Mercury

and this sample musn't comlie too.

I tried to achieve it in the following ways:

1. Modular constraint. I have module

module Sample.Types.Boxes
  ( Substance(..)
  , dangerousBox
  , VDangerousBox {- no Con-}
  ) where

data Substance
  = Uranus
  | Mercury
  | Ammonia
  deriving (Show)

data VDangerousBox a =
  VDangerousBox Substance
  deriving (Show)

dangerousBox :: Substance -> VDangerousBox Substance
dangerousBox a = VDangerousBox a

Clients of module can use only dangerousBox, but here i have jeneric in relation to Substance:

uranus :: VDangerousBox Substance
uranus = dangerousBox Uranus

2. Data kinds

data DangerousBox :: Substance -> * where
  DangerousBox :: Substance -> DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox Uranus

mercury :: DangerousBox Mercury
mercury = uranus {- it's ok, it dosn't compile -}

But in this case the following case will compile:

mercury :: DangerousBox Mercury
mercury = DangerousBox Ammonia

I understand that i received equivalent for

data Box<T : Substance>(val value: Substance)

in term of Kotlin generics it.

It's no real case, it is only of "academic" interest.

CodePudding user response：

Since, given a particular choice of substance, there isn't any other information to be contained in the box (at least in your Kotlin code), I'd first consider just omitting it entirely:

import Data.Kind (Type)  -- preferred version instead of the old *

data DangerousBox :: Substance -> Type where
  DangerousBox :: DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox

Then the mercury = DangerousBox Ammonia problem can't even arise, because the DangerousBox value constructor doesn't take any arguments.

If for some reason you do need an actual value representing the tag-type, then this should not be the tag itself as a Type-value, because in that view Uranus, Mercury and Ammonia are all the same type. Instead, you should use what's normally called the singletons of these types. You could have them auto-generated, or define them manually:

data SubstanceSing :: Substance -> Type where
  UranusS :: SubstanceSing 'Uranus
  MercuryS :: SubstanceSing 'Mercury
  AmmoniaS :: SubstanceSing 'Ammonia

Now UranusS corresponds to your Kotlin Substance.Uranus when appearing on the value-level. Your box type then becomes

data DangerousBox :: Substance -> Type where
  DangerousBox :: SubstanceSing a -> DangerousBox a

CodePudding user response：

Note that it doesn't really work this way to translate this Kotlin code directly to Haskell, since they have very different type systems. You will most definitely end up with very bad Haskell code. But anyway, since this is for "academic" purposes, I'll continue.

In Kotlin, Uranus, Mercury, Ammonia are all different types, and the behaviour you want to approximate depends on this fact, so it would help if they are also different types in Haskell. On the other hand, Substance can be a type class.

class Substance a
data Uranus = Uranus
data Mercury = Mercury
data Ammonia = Ammonia
instance Substance Uranus 
instance Substance Mercury 
instance Substance Ammonia

DangerousBox could be defined as a newtype:

newtype DangerousBox a = DangerousBox a

Note that a isn't constrained to Substance, like it is in Kotlin. If you really want it, you can enable the deprecated language extension DatatypeContexts.

{-# LANGUAGE DatatypeContexts #-}
newtype (Substance a) => DangerousBox a = DangerousBox a

Then this will compile:

uranus :: DangerousBox Uranus
uranus = DangerousBox Uranus

and these won't:

uranus :: DangerousBox Uranus
uranus = DangerousBox Mercury
-- or
-- uranus = DangerousBox Ammonia