Support nominally distinct Haskell types with identical copilot types

[avieth]

Motivation

It would be great to have domain-specific Haskell types in streams, as this can give extra type safety in the high-level model that, with correct code generation, holds true even in the less-strongly-typed target language. Take this simple example with three nominally and semantically distinct types with the same representation:

-- Three distinct notions, each of which is a 32-bit unsigned integer.
newtype Time_ms = Time_ms { getTime :: Word32 }
newtype Speed_mm_s = Speed_mm_s { getSpeed :: Word32 }
newtype Position_mm = Position_mm { getPosition :: Word32 }

-- In this model, it's more difficult for the programmer to make a mistake, and the
-- type automatically documents the arguments.
some_stream :: Stream Time_ms -> Stream Speed_mm_s -> Stream Position_mm

-- Contrast with this
some_stream_worse :: Stream Word32 -> Stream Word32 -> Stream Word32

I've judged that this is not possible presently, simply because of the definition of Typed

class (Show a, Typeable a) => Typed a where
  typeOf     :: Type a
  ...

data Type :: * -> * where
  Bool    :: Type Bool
  Int8    :: Type Int8
  Int16   :: Type Int16
  Int32   :: Type Int32
  Int64   :: Type Int64
  Word8   :: Type Word8
  Word16  :: Type Word16
  Word32  :: Type Word32
  Word64  :: Type Word64
  Float   :: Type Float
  Double  :: Type Double
  Array   :: forall n t. ( KnownNat n
                         , Typed t
                         , Typed (InnerType t)
                         , Flatten t (InnerType t)
                         ) => Type t -> Type (Array n t)
  Struct  :: (Typed a, Struct a) => a -> Type a

To get Typed Time_ms, for example, you need to give a Type Time_ms, but there is no such thing: it's not a struct or an array, it's a Word32, but the type parameter must be Time_ms.

How could it be done

Needless to say, this would be a massively breaking change worthy of a new major version number.

The idea is to define a kind for types in the object language (Haskell being the meta language) and use this to parameterize Haskell types which represent the object language types and values of those types. The Typed class would then become (ignore bad choice of names)

class CTyped t where
  type CTypeOf t :: CType
  cTypeOf  :: proxy t -> CTypeRep (CTypeOf t)
  cValueOf :: t -> CValRep (CTypeOf t)

and we could get this for our example

instance CTyped Time_ms where
  type CTypeOf Time_ms = CWord32
  cTypeOf _ = 'CTUInt32
  cValueOf (Time_ms t) = CUInt32 t

Here's what CType, CTypeRep, and CValRep could be (as a bonus, we also get support union and enum types)

-- Kinds for names (found in structs, unions, enums) and array length (which
-- must be known statically).
type Name = Symbol
type Length = Nat

-- | A named thing, useful for structs, unions, and even enums.
data CField t where
  CField :: Name -> t -> CField t

-- | Parameter for the enum CField used in CTEnum: only a name is needed.
data CVariant = CVariant

-- | A kind for C type without pointers (see DataKinds extension).
data CType where
  CTBool   :: CType
  CTUInt8  :: CType
  CTUInt16 :: CType
  CTUInt32 :: CType
  CTUInt64 :: CType
  CTInt8   :: CType
  CTInt16  :: CType
  CTInt32  :: CType
  CTInt64  :: CType
  CTArray  :: CType -> Length -> CType
  -- | A type name and named CType fields. Could use NonEmpty to eliminate
  -- empty structs.
  CTStruct :: Name  -> [CField CType] -> CType
  -- | Like struct but for a union. Again, could use NonEmpty.
  CTUnion  :: Name  -> [CField CType] -> CType
  -- | With enums, all you can do is test for equality. Underlying
  -- representation will indeed be an enum but it shall be up to the C compiler
  -- to decide how big it is in memory. The feilds thus are only names, the
  -- type information is not relevant.
  CTEnum   :: Name  -> [CField CVariant] -> CType

-- | Term-level representation of a C type.
data CTypeRep (ty :: CType) where
  CBool_t   :: CTypeRep 'CTBool
  CUInt8_t  :: CTypeRep 'CTUInt8
  CUInt16_t :: CTypeRep 'CTUInt16
  CUInt32_t :: CTypeRep 'CTUInt32
  CUInt64_t :: CTypeRep 'CTUInt64
  CInt8_t   :: CTypeRep 'CTInt8
  CInt16_t  :: CTypeRep 'CTInt16
  CInt32_t  :: CTypeRep 'CTInt32
  CInt64_t  :: CTypeRep 'CTInt64
  -- | For an array we know the length from the type, we only need to give the
  -- type rep for the array elements.
  CArray_t  :: CTypeRep ty -> CTypeRep ('CTArray ty len)
  -- | For a struct we have to give the type rep for each member, in order.
  CStruct_t :: All fields CTypeRep -> CTypeRep ('CTStruct name fields)
  -- | For a union, same as for struct.
  CUnion_t  :: All variants CTypeRep -> CTypeRep ('CTUnion name variants)
  -- | The enum type rep just needs a list of names, no type reps (the type of
  -- an enum variant is intended to be opaque).
  CEnum_t   :: All variants CVariantTypeRep -> CTypeRep ('CTEnum name variants)

data CVariantTypeRep (ty :: CVariant) where
  CVariantTypeRep :: CVariantTypeRep 'CVariant

-- | Term-level representation of a C value.
data CValRep (ty :: CType) where
  CBool   :: Bool   -> CValRep 'CTBool
  CUInt8  :: Word8  -> CValRep 'CTUInt8
  CUInt16 :: Word16 -> CValRep 'CTUInt16
  CUInt32 :: Word32 -> CValRep 'CTUInt32
  CUInt64 :: Word64 -> CValRep 'CTUInt64
  CInt8   :: Int8   -> CValRep 'CTInt8
  CInt16  :: Int16  -> CValRep 'CTInt16
  CInt32  :: Int32  -> CValRep 'CTInt32
  CInt64  :: Int64  -> CValRep 'CTInt64
  CArray  :: Vec len (CValRep ty) -> CValRep ('CTArray ty len)
  CStruct :: All fields CValRep   -> CValRep ('CTStruct name fields)
  CUnion  :: One variants CValRep -> CValRep ('CTUnion name variants)
  CEnum   :: One variants CVariantRep -> CValRep ('CTEnum name variants)

data CVariantRep t where
  CVariantRep :: CVariantRep t

data Vec (len :: Length) t where
  VNil  :: Vec 0 t
  VCons :: t -> Vec n t -> Vec (n + 1) t

data All (fields :: [CField t]) (f :: t -> Kind.Type) where
  None :: All '[] f
  More :: f t -> All fields f -> All ('CField name t ': fields) f

data One (variants :: [CField t]) (f :: t -> Kind.Type) where
  Here  :: f t -> One ('CField name t ': variants) f
  There :: One ts f -> One (t ': ts) f

-- We would need to be able to produce a C type declaration from a
-- CType, and a C value of that type from a corresponding CVal.

class CTyped t where
  type CTypeOf t :: CType
  cTypeOf  :: proxy t -> CTypeRep (CTypeOf t)
  cValueOf :: t -> CValRep (CTypeOf t)

instance CTyped Word8 where
  type CTypeOf Word8 = 'CTUInt8
  cTypeOf _ = CUInt8_t
  cValueOf = CUInt8

data Foo = Foo { foo :: Word8, bar :: Word8 }

instance CTyped Foo where
  type CTypeOf Foo = 'CTStruct "foo" '[
      'CField "foo" (CTypeOf Word8)
    , 'CField "bar" (CTypeOf Word8)
    ]
  cTypeOf _ = CStruct_t
    $ More (cTypeOf (Proxy :: Proxy Word8))
    $ More (cTypeOf (Proxy :: Proxy Word8))
    $ None
  cValueOf x = CStruct (More (cValueOf (foo x)) (More (cValueOf (bar x)) None))

[fdedden]

This is a feature that is requested before (#56), and something we definitely want to implement. Having this amount of type-safety will really introduce a huge benefit over using C.

Indeed Type is the main obstacle in implementing this. When this is solved, we can easily use generics to deriving instances for said types.

With the limited time we can currently spent on developing Copilot, we focus mostly on bugfixing and cleaning the project up. Copilot's types are one of the things that we want to try to simplify, most likely aiding in implementing more strict types.

[ivanperez-keera]

Although the approach is different, this issue is closely related to #56 and solving this one would solve that one too. i have closed #56, but it may actually be a good starting point and should be considered if some additional type safety feature is to be implemented.

[jeannekamikaze]

I'm too noob to make any meaningful contribution in this space. How are you making up for the lack of Haskell types currently? It seems that Copilot programs currently are forced to use the C types defined in Type. Is there some way, for example, to (maybe unsafely) cast a Haskell Enum to a Word32?

[ivanperez-keera]

Sorry, but wouldn't it be possible to do something like this?

class (Show a, Typeable a, Reducible a b) => Typed a where
  typeOf :: Type b

Where the binary class Reducible represents a relation between types that have the same representation as another type?

Then you could say that any type can be reduced to itself, and a new type would only need to define an instance saying that it can be reduced to the type it encloses?

EDIT: Reducible sort of captures the idea of an isomorphism, but it would be used such that the type checker will try to pick the final type representation without ending up in some loop.

[ivanperez-keera]

We may want to look into https://hackage.haskell.org/package/base-4.14.1.0/docs/Data-Coerce.html#t:Coercible.

We might be able to provide instances for Typed for any type that can be coerced to another type if we change the class to:

class (Show b, Typeable b, Coercible a b) => Typed a b where
  typeOf :: Type b

[ivanperez-keera]

By the way, I have no idea why we require the Typeable and Show instances, but that often leads to very confusing error messages when there are type errors (like saying that something's doesn't type check because the compiler can't provide a Show instance for it).

[ivanperez-keera]

I wasn't able to get the Coercible trick work. If someone wants to give this a try, please feel free.

[ivanperez-keera]

Tagging @avieth . Maybe he knows. There may be a way to simplify his solution using Coercibles, I don't know.