Type Declarations in Unison

data DataDeclaration' v a = DataDeclaration {
  annotation :: a,
  bound :: [v],
  constructors' :: [(a, v, AnnotatedType v a)]
  -- isStructural :: IsStructural
  -- isOpaque :: Set (AnnotatedTerm v a)
} deriving (Eq, Show, Functor)

-- type IsStructural = Structural | Unique GUID

Structural Types

Structural types are defined uniquely by their structure. Every constructor has a unique signature, which intrinsically defines the meaning of the constructor. For example, the following types are identical and interoperable:

structural type Maybe a = Nothing | Just a
structural type Optional t = Some t | None

These definitions would also be identical and interoperable (although they maybe shouldn't be):

structural type Validation e a = Success a | Failure e
structural type Either a b = Left a | Right b

It should be an error if two constructors of a structural type have the same signature, indicating that the semantics are defined outside of the structure.

The identity of a structural type is determined by normalizing the constructor order by <todo: explain how> and then hashing their types.

Unique types

Unique types are have extrinsic semantics, not completely defined by the constructor types. Their representation includes a GUID, along with the constructors. The constructors types need not be unique. The GUID is typically auto-generated, but can be specified as part of the type declaration, in order to use a textual representation to declare an identical type.

unique type Day = Mon | Tue | Wed | ...

unique[<guid>]
type Day = Mon | Tue | Wed | ...

Order of constructors having the same type is stable, but the relative constructor order of differently typed constructors is (currently) unspecified.

Opaque Types

An opaque type has a structure and a block of terms that can inspect structure. The hash of those terms is part of the type ID. They have a flag in the decl so typechecker can prevent access.

opaque type Socket = Socket Nat
opaque type Handle = Handle Text

Q: How do you declare a definition that can inspect two opaque types? Q: How do we create and inspect Sockets? We don't want to create public accessors, but we do want some way for privileged code to construct those values. I guess it's straightforward for types with a single constructor, but we may end up needing some deterministic way of distinguishing the other constructors.

For reference and comparison: https://docs.scala-lang.org/sips/opaque-types.html Notes re Scala opaque types:

They are a type alias (no boxing) that is only equal for definitions inside a corresponding companion object/module.
We (Unison) do need to "box" values within a constructor to give them a hash corresponding to their type identity.

Combinations?

Structural + Unique: No. Structural + Opaque: No. Unique + Opaque: Sure why not. Example where you want Opaque without Unique: SortedSet -- the exposed methods define the semantics. Example where you want Unique + Opaque: Socket, Handle -- the exposed methods may necessarily dictate that the two types are not the same.

Misc scenarios / questions:

I was just editing some Haskell code.

-- InputPatterns accept some fixed number of Required arguments of various
-- types, followed by a variable number of a single type of argument.
data IsOptional
  = Optional -- 0 or 1, at the end
  | Required -- 1, at the start
  | ZeroPlus -- 0 or more, at the end
  | OnePlus -- 1 or more, at the end
  deriving Show

I decided to move Required to the top for clarity since, as the comments state, InputPattern arg lists start with some number of Required arguments.

data IsOptional
  = Optional -- 0 or 1, at the end
  | Required -- 1, at the start
  | ZeroPlus -- 0 or more, at the end
  | OnePlus -- 1 or more, at the end
  deriving Show

I still want this to be the same type. None of the semantics have changed, I just reordered the constructors for readability. I don't think this would be possible with any of our current proposed type implementations. Yes, I could create a new unique type, and refactor everything to use that, but that strikes me as unappealing, especially from a code-sharing perspective.

Thoughts?

@pchiusano - I'd say that "constructor display order" should be a bit of metadata that can be attached to a data declaration, and you should be able to edit this metadata somehow (perhaps by default, the add / update command can suggest "metadata edits" in reponse to this sort of thing).

Old stuff: Algebraic Types?

Algebraic types are defined by their structure and a set of laws relating their fields. Note that the laws may involve more than one type.

algebraic Monoid a = Monoid { mempty : a, mappend : a -> a -> a }
where m a -> (mappend m) (mempty m) a == a
      m a -> (mappend m) a (mempty m) == a
      m a b c -> (mappend m) a ((mappend m) b c) ==
                 (mappend m) ((mappend m) a b) c

5.0 KiB Raw Blame History