Skip to content

Instantly share code, notes, and snippets.

@mizunashi-mana
Created January 12, 2020 10:34
Show Gist options
  • Save mizunashi-mana/4522da17c8ade08b3376b1596c06be72 to your computer and use it in GitHub Desktop.
Save mizunashi-mana/4522da17c8ade08b3376b1596c06be72 to your computer and use it in GitHub Desktop.
An idea of new programming language
module Main where
dict Integral a = Integral {
fromInteger: Integer -> a,
+: a -> a -> a,
-: a -> a -> a,
iszero: a -> Bool,
}
impl integralForInteger: Integral Integer
integralForInteger = Integral have
fromInteger x = x
x + y = x Main.+ y
x - y = x Main.- y
iszero = \
0 -> True
_ -> False
fromInteger: forall a. Integral a => Integer -> a
fromInteger %d = d.fromInteger
module Fib begin
fib: forall a. Integral a => a -> a
fib @a %d n = go n a0 a1
where
a0 = fromInteger %integralForInteger 0
a1 = fromInteger 1 -- implicit dictionary inference
-- `go` can have a signature `go: a -> a -> a -> a`
go m x y = \
| d.iszero m -> x
| else -> go (m - 1) y (x d.+ y)
end
main: IO ()
main = print $ Fib.fib 10
@TheMatten
Copy link

@Icelandjack What about ditching typeclasses altogether and instead introducing implicit arguments (provided through =>) and "hints"?:

module Main where

newtype Integral a = Integral
  { fromInteger :: Integer -> a
  , (+)         :: a -> a -> a
  , (-)         :: a -> a -> a
  , isZero      :: a -> Bool
  }

-- These could be done with some sugar or TH:
-- (plus, let's say we've already switched to anonymous record just for kicks)
fromInteger :: Integral a => Integer -> a
fromInteger %(Integral d) = d.fromInteger

..

-- Reusing "default" keyword, could be "auto" or "hint"
default integralInteger :: Integral Integer
integralInteger = Integral
  { fromInteger = id
  , (+)         = plusInteger
  , (*)         = timesInteger
  , isZero      = \case
      0 -> True
      _ -> False
  }

@mizunashi-mana
Copy link
Author

@TheMatten This idea is nice. However, some points to introduce special dictionary type; I will make this syntax be introduced as syntactic sugar for datatype declaration.

  • This language will be strict. Then,

    newtype A = A
      { a :: Int
      }
    
    default defaultA :: A
    defaultA = A
      { a = undefined
      }
    
    f :: A => ()
    f = ()
    
    main = pure f

    should panic? And, if f declaration is missing and main = pure (), one should panic? There are several ways we can choose.

  • There are many methods to solve the instance of implicit argument, and each method require each costraint of instance forms to decide the argument safely and efficiently.

In other words, dictionary type is different from usual data type at the some points(, and it is same as module type actually). Because different objects should have different representation on language, dict keyword was introduced.

I agree with current language design has some wrong which can improved. I will improve this.

@TheMatten
Copy link

@mizunashi-mana

  • similarly to how typeclasses work in strict languages (like Purescript), I would expect (and thus want) them to behave the same way as normal arguments - thus pure f should diverge, because it get's resolved to pure (f %defaultA), similarly to how this should:
f' :: A -> ()
f' _ = ()

main = pure (f' defaultA)
  • not sure what you mean, but I don't think dictionary is in any way different from normal data type - in Haskell, it isn't internally either and there're even thoughts about allowing explicit dictionary passing and removing Constraint kind.

@TheMatten
Copy link

TheMatten commented Jan 12, 2020

BTW, such system should be as powerful as typeclasses are - you could have superclasses by having constraints on default value:

default monoidMaybe :: Monoid a => Monoid (Maybe a)

Plus, you could have overlapping instances by introducing overlapping mechanism similar to HS, or possibly using dependent types:

default fooIntOrElse :: foreach a. Foo a
fooIntOrElse = case a of
  Int -> ..
  _   -> ..

@mizunashi-mana
Copy link
Author

mizunashi-mana commented Jan 12, 2020

@TheMatten

  • In strict language (this is not Haskell with Strict extension), this may be not diverge.

    f :: ()
    f = undefined

    but this should be diverge

    main = pure f

    If we see type classes as implicit module, this may not be diverge similary

    dict A = A { a :: () }
    
    default defA :: A
    defA = A { a = undefined }
    
    f :: A => ()
    f %d = %d `seq` ()
    
    main = pure $ f %defA

    but this should be diverge

    f :: A => ()
    f %d = %d.a
    
    main = pure $ f %defA

    If we expect dictionary as data type, both should be diverge. But if we expect dictionary as module, first case should be not diverge. This discussion is also opened on GHC especially about unlifted data type. Now, GHC's class constraint is always lifted to avoid this discussion.

  • I agree with dictionary is normal data type internally. However, on language, dictionary instance form may lead undecidability for constraint solving method. So, Haskell require strict instance form; we can relax this constraint using some GHC extensions. Moreover, if constraint solving method is decidable for all instance form, performance of it is too bad. Therefore, we should restrict dictionary type and instance form similar to Haskell.

@TheMatten
Copy link

  • In strict language (this is not Haskell with Strict extension), this may be not diverge.
f :: ()
f = undefined

This diverges - when it's used somewhere.

but this should be diverge

main = pure f

Yes.

If we see type classes as implicit module, this may not be diverge similary

dict A = A { a :: () }

default defA :: A
defA = A { a = undefined }

f :: A => ()
f %d = %d `seq` ()

main = pure $ f %defA

This main should - in strict language, A { a = undefined } = A undefined = undefined, so in pure $ f %defA, you're basically passing undefined into f - just the fact that it's passed here as an argument is reason for it to panic. BTW, in strict language, seq should be no-op - you never get thunk to evaluate, argument of some type a is evaluated value of such type, not a computation that produces it.

When it comes to decidability in instance search, it isn't really that useful in non-total language - if it gets stuck, it will happen at compile-time, not runtime, plus we're already disabling it in Haskell in many cases.

@mizunashi-mana
Copy link
Author

mizunashi-mana commented Jan 13, 2020

@TheMatten

in strict language, A { a = undefined } = A undefined = undefined, so in pure $ f %defA, you're basically passing undefined into f - just the fact that it's passed here as an argument is reason for it to panic.

This is not the unique solution and I expect A { a = undefined } is a normal form as Main { f = undefined } is not diverge if A is a dictionary constructor (module constructor).

When it comes to decidability in instance search, it isn't really that useful in non-total language

In many cases, decidability in instance search is related compile performance directly. I agree with it isn't useful for language user. However, it is important for language provider because instance search may be bottleneck. And, it is a choice to restrict instance form for compile performance although it may make language power is weaker.

@TheMatten
Copy link

This is not the unique solution and I expect A { a = undefined } is a normal form as Main { f = undefined } is not diverge if A is a dictionary constructor (module constructor).

Alright, so you want modules/dictionaries to behave in a specific way. Yeah, then they aren't ordinary values after all.

In many cases, decidability in instance search is related compile performance directly. I agree with it isn't useful for language user. However, it is important for language provider because instance search may be bottleneck. And, it is a choice to restrict instance form for compile performance although it may make language power is weaker.

Part of GHC's manual about overlapping instances describes how instance search works in GHC, plus part about UndecidableInstances mentions that it's used to lift "rules that ensure that instance resolution will terminate". I don't see any mention about performance effect in either of these, neither I'm sure how ensuring termination of instance search can help performance directly - but maybe you can point me to some useful material.

@mizunashi-mana
Copy link
Author

@TheMatten

In many cases, algorithms for undecidable problem are unpredictable; this is from my experience and not principle.

In many cases, decidability in instance search is related compile performance directly.

may have mistake, sorry. Correctly, guarantee of decidability of instance search is important for language designer to maintain the compiler.

Decidability of instance search is more generic concept. A group of instances with cyclic super context is just one of undecidability. Haskell have special syntax for class and instance declaration and the designers of the language thought decidability of instance resolution deeply. Then, undecidable problem of instance resolution in Haskell is just "cyclic context". However, we can choose another design that the instance resolution of our language is turing complete (e.g. arithmetic expression is allowed). This is expressive but compile time depends strongly on the program.

Scala has powerful instance searcher which is a solution of undecidable problem. However, it is a troublemaker for compile performance.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment