AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Generalise abstract dynamic entity types #244

Closed AshleyYakeley closed 5 months ago

AshleyYakeley commented 11 months ago

Concrete dynamic type: "dynamictype" <type-const> "=" <anchor>

Abstract dynamic type: "dynamictype" <type-const>

Then use subtype relations to define abstract dynamic types.

subtype Q <: P where Q is a concrete dynamic type and P is an abstract dynamic type.

Downside: same code is accepted in different scopes, but with different results:

dynamictype P;
dynamictype Q = !"Q";

t1 = check @P (point.DynamicEntity @Q !"x")

t2 = let subtype Q <: P in check @P (point.DynamicEntity @Q !"x")
AshleyYakeley commented 8 months ago

Alternative: define subtype relations at time of concrete creation.

dynamictype P;
dynamictype Q = !"Q" <: P;

This wouldn't work:

let
dynamictype P;
q: DynamicEntity = let dynamictype Q = !"Q" <: P in point.DynamicEntity @Q !"q";
in check @P q
AshleyYakeley commented 6 months ago

"same code is accepted in different scopes, but with different results" is already a thing in Haskell, sort of:

{-# LANGUAGE
    CPP,
    TypeApplications,
    FlexibleInstances,
    AllowAmbiguousTypes
#-}

#define FLAG 1

module Main where

import Prelude

class C x where
    val :: Int

instance C (Maybe a) where
    val = 1

#if FLAG
instance {-# OVERLAPPING #-} C (Maybe ()) where
    val = 2
#endif

main :: IO ()
main = putStrLn $ show (val @(Maybe ()))
AshleyYakeley commented 6 months ago

Should subtype relationships be inferred when not declared?

For example:

dynamictype P;
dynamictype Q;
dynamictype X = !"X";
subtype X <: Q;

Does this give P <: Q even though this is not declared?

Prefer "no"

AshleyYakeley commented 5 months ago

Done.